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	⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 )
Assertion	mh-inf3sn	⊢ ω ∈ V

Proof

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