Theorem onsucsuccmpi

Description: The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015)

	Ref	Expression
Hypothesis	onsucsuccmpi.1	⊢ 𝐴 ∈ On
Assertion	onsucsuccmpi	⊢ suc suc 𝐴 ∈ Comp

Proof

Step	Hyp	Ref	Expression
1		onsucsuccmpi.1	⊢ 𝐴 ∈ On
2	1	onsuci	⊢ suc 𝐴 ∈ On
3		onsuctop	⊢ ( suc 𝐴 ∈ On → suc suc 𝐴 ∈ Top )
4	2 3	ax-mp	⊢ suc suc 𝐴 ∈ Top
5	1	onirri	⊢ ¬ 𝐴 ∈ 𝐴
6	1 1	onsucssi	⊢ ( 𝐴 ∈ 𝐴 ↔ suc 𝐴 ⊆ 𝐴 )
7	5 6	mtbi	⊢ ¬ suc 𝐴 ⊆ 𝐴
8		sseq1	⊢ ( suc 𝐴 = ∪ 𝑦 → ( suc 𝐴 ⊆ 𝐴 ↔ ∪ 𝑦 ⊆ 𝐴 ) )
9	7 8	mtbii	⊢ ( suc 𝐴 = ∪ 𝑦 → ¬ ∪ 𝑦 ⊆ 𝐴 )
10		elpwi	⊢ ( 𝑦 ∈ 𝒫 suc 𝐴 → 𝑦 ⊆ suc 𝐴 )
11	10	unissd	⊢ ( 𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦 ⊆ ∪ suc 𝐴 )
12	1	onunisuci	⊢ ∪ suc 𝐴 = 𝐴
13	11 12	sseqtrdi	⊢ ( 𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦 ⊆ 𝐴 )
14	9 13	nsyl	⊢ ( suc 𝐴 = ∪ 𝑦 → ¬ 𝑦 ∈ 𝒫 suc 𝐴 )
15		eldif	⊢ ( 𝑦 ∈ ( 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } ) ∖ 𝒫 suc 𝐴 ) ↔ ( 𝑦 ∈ 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } ) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴 ) )
16		elpwunsn	⊢ ( 𝑦 ∈ ( 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } ) ∖ 𝒫 suc 𝐴 ) → suc 𝐴 ∈ 𝑦 )
17	15 16	sylbir	⊢ ( ( 𝑦 ∈ 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } ) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴 ) → suc 𝐴 ∈ 𝑦 )
18	17	ex	⊢ ( 𝑦 ∈ 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } ) → ( ¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦 ) )
19		df-suc	⊢ suc suc 𝐴 = ( suc 𝐴 ∪ { suc 𝐴 } )
20	19	pweqi	⊢ 𝒫 suc suc 𝐴 = 𝒫 ( suc 𝐴 ∪ { suc 𝐴 } )
21	18 20	eleq2s	⊢ ( 𝑦 ∈ 𝒫 suc suc 𝐴 → ( ¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦 ) )
22		snelpwi	⊢ ( suc 𝐴 ∈ 𝑦 → { suc 𝐴 } ∈ 𝒫 𝑦 )
23		snfi	⊢ { suc 𝐴 } ∈ Fin
24	23	jctr	⊢ ( { suc 𝐴 } ∈ 𝒫 𝑦 → ( { suc 𝐴 } ∈ 𝒫 𝑦 ∧ { suc 𝐴 } ∈ Fin ) )
25		elin	⊢ ( { suc 𝐴 } ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( { suc 𝐴 } ∈ 𝒫 𝑦 ∧ { suc 𝐴 } ∈ Fin ) )
26	24 25	sylibr	⊢ ( { suc 𝐴 } ∈ 𝒫 𝑦 → { suc 𝐴 } ∈ ( 𝒫 𝑦 ∩ Fin ) )
27	2	elexi	⊢ suc 𝐴 ∈ V
28	27	unisn	⊢ ∪ { suc 𝐴 } = suc 𝐴
29	28	eqcomi	⊢ suc 𝐴 = ∪ { suc 𝐴 }
30		unieq	⊢ ( 𝑧 = { suc 𝐴 } → ∪ 𝑧 = ∪ { suc 𝐴 } )
31	30	rspceeqv	⊢ ( ( { suc 𝐴 } ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ suc 𝐴 = ∪ { suc 𝐴 } ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 )
32	26 29 31	sylancl	⊢ ( { suc 𝐴 } ∈ 𝒫 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 )
33	22 32	syl	⊢ ( suc 𝐴 ∈ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 )
34	14 21 33	syl56	⊢ ( 𝑦 ∈ 𝒫 suc suc 𝐴 → ( suc 𝐴 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 ) )
35	34	rgen	⊢ ∀ 𝑦 ∈ 𝒫 suc suc 𝐴 ( suc 𝐴 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 )
36	2	onunisuci	⊢ ∪ suc suc 𝐴 = suc 𝐴
37	36	eqcomi	⊢ suc 𝐴 = ∪ suc suc 𝐴
38	37	iscmp	⊢ ( suc suc 𝐴 ∈ Comp ↔ ( suc suc 𝐴 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 suc suc 𝐴 ( suc 𝐴 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) suc 𝐴 = ∪ 𝑧 ) ) )
39	4 35 38	mpbir2an	⊢ suc suc 𝐴 ∈ Comp