Theorem: SetTheory.succ_mem_ω (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : n ∈ ω
⊢ succ n ∈ ω
Tactic:
rw [mem_ω_iff] at hn ⊢
State after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
⊢ ∀ (s : V), Inductive s → succ n ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
⊢ ∀ (s : V), Inductive s → succ n ∈ s
Tactic:
intro s hs
State after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
s : V
hs : Inductive s
⊢ succ n ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
s : V
hs : Inductive s
⊢ succ n ∈ s
Tactic:
exact hs.succ_mem n (hn s hs)
State after:
no goals