Metamath Proof Explorer

Theorem mh-inf3sn

Description: Version of inf3 for the set of Zermelo ordinals (/) , { (/) } , { { (/) } } , { { { (/) } } } , etc., where the successor of y is { y } . Unlike inf3 , the proof does not require ax-reg , since the singleton properties snnz and sneqr are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Hypothesis mh-inf3sn.1 ⊢ ∃ x ∅ ∈ x ∧ ∀ y ∈ x y ∈ x
Assertion mh-inf3sn ⊢ ω ∈ V

Proof

Step Hyp Ref Expression
1 mh-inf3sn.1 ⊢ ∃ x ∅ ∈ x ∧ ∀ y ∈ x y ∈ x
2 simpr ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → ∀ y ∈ x y ∈ x
3 vex ⊢ y ∈ V
4 3 sneqr ⊢ y = z → y = z
5 4 rgen2w ⊢ ∀ y ∈ x ∀ z ∈ x y = z → y = z
6 eqid ⊢ y ∈ x ⟼ y = y ∈ x ⟼ y
7 sneq ⊢ y = z → y = z
8 6 7 f1mpt ⊢ y ∈ x ⟼ y : x ⟶ 1-1 x ↔ ∀ y ∈ x y ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y = z → y = z
9 2 5 8 sylanblrc ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → y ∈ x ⟼ y : x ⟶ 1-1 x
10 simpl ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → ∅ ∈ x
11 snnzg ⊢ y ∈ x → y ≠ ∅
12 11 necomd ⊢ y ∈ x → ∅ ≠ y
13 12 neneqd ⊢ y ∈ x → ¬ ∅ = y
14 13 nrex ⊢ ¬ ∃ y ∈ x ∅ = y
15 vsnex ⊢ y ∈ V
16 6 15 elrnmpti ⊢ ∅ ∈ ran ⁡ y ∈ x ⟼ y ↔ ∃ y ∈ x ∅ = y
17 14 16 mtbir ⊢ ¬ ∅ ∈ ran ⁡ y ∈ x ⟼ y
18 17 a1i ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → ¬ ∅ ∈ ran ⁡ y ∈ x ⟼ y
19 10 18 eldifd ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → ∅ ∈ x ∖ ran ⁡ y ∈ x ⟼ y
20 9 19 mh-inf3f1 ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → rec ⁡ y ∈ x ⟼ y ∅ ↾ ω : ω ⟶ 1-1 x
21 vex ⊢ x ∈ V
22 f1dmex ⊢ rec ⁡ y ∈ x ⟼ y ∅ ↾ ω : ω ⟶ 1-1 x ∧ x ∈ V → ω ∈ V
23 20 21 22 sylancl ⊢ ∅ ∈ x ∧ ∀ y ∈ x y ∈ x → ω ∈ V
24 23 1 exlimiiv ⊢ ω ∈ V