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	|- A e. On
Assertion	onsucsuccmpi	|- suc suc A e. Comp

Proof

Step	Hyp	Ref	Expression
1		onsucsuccmpi.1	|- A e. On
2	1	onsuci	|- suc A e. On
3		onsuctop	|- ( suc A e. On -> suc suc A e. Top )
4	2 3	ax-mp	|- suc suc A e. Top
5	1	onirri	|- -. A e. A
6	1 1	onsucssi	|- ( A e. A <-> suc A C_ A )
7	5 6	mtbi	|- -. suc A C_ A
8		sseq1	|- ( suc A = U. y -> ( suc A C_ A <-> U. y C_ A ) )
9	7 8	mtbii	|- ( suc A = U. y -> -. U. y C_ A )
10		elpwi	|- ( y e. ~P suc A -> y C_ suc A )
11	10	unissd	|- ( y e. ~P suc A -> U. y C_ U. suc A )
12	1	onunisuci	|- U. suc A = A
13	11 12	sseqtrdi	|- ( y e. ~P suc A -> U. y C_ A )
14	9 13	nsyl	|- ( suc A = U. y -> -. y e. ~P suc A )
15		eldif	|- ( y e. ( ~P ( suc A u. { suc A } ) \ ~P suc A ) <-> ( y e. ~P ( suc A u. { suc A } ) /\ -. y e. ~P suc A ) )
16		elpwunsn	|- ( y e. ( ~P ( suc A u. { suc A } ) \ ~P suc A ) -> suc A e. y )
17	15 16	sylbir	|- ( ( y e. ~P ( suc A u. { suc A } ) /\ -. y e. ~P suc A ) -> suc A e. y )
18	17	ex	|- ( y e. ~P ( suc A u. { suc A } ) -> ( -. y e. ~P suc A -> suc A e. y ) )
19		df-suc	|- suc suc A = ( suc A u. { suc A } )
20	19	pweqi	|- ~P suc suc A = ~P ( suc A u. { suc A } )
21	18 20	eleq2s	|- ( y e. ~P suc suc A -> ( -. y e. ~P suc A -> suc A e. y ) )
22		snelpwi	|- ( suc A e. y -> { suc A } e. ~P y )
23		snfi	|- { suc A } e. Fin
24	23	jctr	|- ( { suc A } e. ~P y -> ( { suc A } e. ~P y /\ { suc A } e. Fin ) )
25		elin	|- ( { suc A } e. ( ~P y i^i Fin ) <-> ( { suc A } e. ~P y /\ { suc A } e. Fin ) )
26	24 25	sylibr	|- ( { suc A } e. ~P y -> { suc A } e. ( ~P y i^i Fin ) )
27	2	elexi	|- suc A e. _V
28	27	unisn	|- U. { suc A } = suc A
29	28	eqcomi	|- suc A = U. { suc A }
30		unieq	|- ( z = { suc A } -> U. z = U. { suc A } )
31	30	rspceeqv	|- ( ( { suc A } e. ( ~P y i^i Fin ) /\ suc A = U. { suc A } ) -> E. z e. ( ~P y i^i Fin ) suc A = U. z )
32	26 29 31	sylancl	|- ( { suc A } e. ~P y -> E. z e. ( ~P y i^i Fin ) suc A = U. z )
33	22 32	syl	|- ( suc A e. y -> E. z e. ( ~P y i^i Fin ) suc A = U. z )
34	14 21 33	syl56	|- ( y e. ~P suc suc A -> ( suc A = U. y -> E. z e. ( ~P y i^i Fin ) suc A = U. z ) )
35	34	rgen	|- A. y e. ~P suc suc A ( suc A = U. y -> E. z e. ( ~P y i^i Fin ) suc A = U. z )
36	2	onunisuci	|- U. suc suc A = suc A
37	36	eqcomi	|- suc A = U. suc suc A
38	37	iscmp	|- ( suc suc A e. Comp <-> ( suc suc A e. Top /\ A. y e. ~P suc suc A ( suc A = U. y -> E. z e. ( ~P y i^i Fin ) suc A = U. z ) ) )
39	4 35 38	mpbir2an	|- suc suc A e. Comp