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 \in On$
	Assertion	onsucsuccmpi	$⊢ suc suc A \in Comp$

Proof

Step	Hyp	Ref	Expression
1		onsucsuccmpi.1	$⊢ A \in On$
2	1	onsuci	$⊢ suc A \in On$
3		onsuctop	$⊢ suc A \in On \to suc suc A \in Top$
4	2 3	ax-mp	$⊢ suc suc A \in Top$
5	1	onirri	$⊢ \neg A \in A$
6	1 1	onsucssi	$⊢ A \in A \leftrightarrow suc A \subseteq A$
7	5 6	mtbi	$⊢ \neg suc A \subseteq A$
8		sseq1	$⊢ suc A = ⋃ y \to (suc A \subseteq A \leftrightarrow ⋃ y \subseteq A)$
9	7 8	mtbii	$⊢ suc A = ⋃ y \to \neg ⋃ y \subseteq A$
10		elpwi	$⊢ y \in 𝒫 suc A \to y \subseteq suc A$
11	10	unissd	$⊢ y \in 𝒫 suc A \to ⋃ y \subseteq ⋃ suc A$
12	1	onunisuci	$⊢ ⋃ suc A = A$
13	11 12	sseqtrdi	$⊢ y \in 𝒫 suc A \to ⋃ y \subseteq A$
14	9 13	nsyl	$⊢ suc A = ⋃ y \to \neg y \in 𝒫 suc A$
15		eldif	$⊢ y \in (𝒫 (suc A \cup \{suc A\}) ∖ 𝒫 suc A) \leftrightarrow (y \in 𝒫 (suc A \cup \{suc A\}) \land \neg y \in 𝒫 suc A)$
16		elpwunsn	$⊢ y \in (𝒫 (suc A \cup \{suc A\}) ∖ 𝒫 suc A) \to suc A \in y$
17	15 16	sylbir	$⊢ (y \in 𝒫 (suc A \cup \{suc A\}) \land \neg y \in 𝒫 suc A) \to suc A \in y$
18	17	ex	$⊢ y \in 𝒫 (suc A \cup \{suc A\}) \to (\neg y \in 𝒫 suc A \to suc A \in y)$
19		df-suc	$⊢ suc suc A = suc A \cup \{suc A\}$
20	19	pweqi	$⊢ 𝒫 suc suc A = 𝒫 (suc A \cup \{suc A\})$
21	18 20	eleq2s	$⊢ y \in 𝒫 suc suc A \to (\neg y \in 𝒫 suc A \to suc A \in y)$
22		snelpwi	$⊢ suc A \in y \to \{suc A\} \in 𝒫 y$
23		snfi	$⊢ \{suc A\} \in Fin$
24	23	jctr	$⊢ \{suc A\} \in 𝒫 y \to (\{suc A\} \in 𝒫 y \land \{suc A\} \in Fin)$
25		elin	$⊢ \{suc A\} \in (𝒫 y \cap Fin) \leftrightarrow (\{suc A\} \in 𝒫 y \land \{suc A\} \in Fin)$
26	24 25	sylibr	$⊢ \{suc A\} \in 𝒫 y \to \{suc A\} \in (𝒫 y \cap Fin)$
27	2	elexi	$⊢ suc A \in V$
28	27	unisn	$⊢ ⋃ \{suc A\} = suc A$
29	28	eqcomi	$⊢ suc A = ⋃ \{suc A\}$
30		unieq	$⊢ z = \{suc A\} \to ⋃ z = ⋃ \{suc A\}$
31	30	rspceeqv	$⊢ (\{suc A\} \in (𝒫 y \cap Fin) \land suc A = ⋃ \{suc A\}) \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z$
32	26 29 31	sylancl	$⊢ \{suc A\} \in 𝒫 y \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z$
33	22 32	syl	$⊢ suc A \in y \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z$
34	14 21 33	syl56	$⊢ y \in 𝒫 suc suc A \to (suc A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z)$
35	34	rgen	$⊢ \forall y \in 𝒫 suc suc A (suc A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z)$
36	2	onunisuci	$⊢ ⋃ suc suc A = suc A$
37	36	eqcomi	$⊢ suc A = ⋃ suc suc A$
38	37	iscmp	$⊢ suc suc A \in Comp \leftrightarrow (suc suc A \in Top \land \forall y \in 𝒫 suc suc A (suc A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) suc A = ⋃ z))$
39	4 35 38	mpbir2an	$⊢ suc suc A \in Comp$

Metamath Proof Explorer

Theorem onsucsuccmpi

Proof