Theorem: SetTheory.mem_ω_iff (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ ω ↔ ∀ (s : V), Inductive s → n ∈ s
Tactic:
unfold ω
State after:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ sep (BoundedFormula.isNat (Sum.inr 0)) (fun i => Empty.elim i) Infinity.inductiveSet ↔
    ∀ (s : V), Inductive s → n ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ sep (BoundedFormula.isNat (Sum.inr 0)) (fun i => Empty.elim i) Infinity.inductiveSet ↔
    ∀ (s : V), Inductive s → n ∈ s
Tactic:
simp only [mem_sep_iff, interpret_isNat', interpret_inr, and_iff_right_iff_imp]
State after:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet
Tactic:
intro hn
State after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (y : V), Inductive y → n ∈ y
⊢ n ∈ Infinity.inductiveSet

State before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (y : V), Inductive y → n ∈ y
⊢ n ∈ Infinity.inductiveSet
Tactic:
exact hn _ Infinity.inductiveSet_inductive
State after:
no goals