Theorem ordcmp

Description: An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1o . (Contributed by Chen-Pang He, 1-Nov-2015)

	Ref	Expression
Assertion	ordcmp	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Comp}\leftrightarrow \left(\bigcup A=\bigcup \bigcup A\to A=1_{𝑜}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		orduni	$$⊢\mathrm{Ord}A\to \mathrm{Ord}\bigcup A$$
2		unizlim	$$⊢\mathrm{Ord}\bigcup A\to \left(\bigcup A=\bigcup \bigcup A\leftrightarrow \left(\bigcup A=\varnothing \vee \mathrm{Lim}\bigcup A\right)\right)$$
3		uni0b	$$⊢\bigcup A=\varnothing \leftrightarrow A\subseteq \left\{\varnothing \right\}$$
4	3	orbi1i	$$⊢\left(\bigcup A=\varnothing \vee \mathrm{Lim}\bigcup A\right)\leftrightarrow \left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)$$
5	2 4	bitrdi	$$⊢\mathrm{Ord}\bigcup A\to \left(\bigcup A=\bigcup \bigcup A\leftrightarrow \left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)\right)$$
6	5	biimpd	$$⊢\mathrm{Ord}\bigcup A\to \left(\bigcup A=\bigcup \bigcup A\to \left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)\right)$$
7	1 6	syl	$$⊢\mathrm{Ord}A\to \left(\bigcup A=\bigcup \bigcup A\to \left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)\right)$$
8		sssn	$$⊢A\subseteq \left\{\varnothing \right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{\varnothing \right\}\right)$$
9		0ntop	$$⊢\neg \varnothing \in \mathrm{Top}$$
10		cmptop	$$⊢\varnothing \in \mathrm{Comp}\to \varnothing \in \mathrm{Top}$$
11	9 10	mto	$$⊢\neg \varnothing \in \mathrm{Comp}$$
12		eleq1	$$⊢A=\varnothing \to \left(A\in \mathrm{Comp}\leftrightarrow \varnothing \in \mathrm{Comp}\right)$$
13	11 12	mtbiri	$$⊢A=\varnothing \to \neg A\in \mathrm{Comp}$$
14	13	pm2.21d	$$⊢A=\varnothing \to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)$$
15		id	$$⊢A=\left\{\varnothing \right\}\to A=\left\{\varnothing \right\}$$
16		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
17	15 16	eqtr4di	$$⊢A=\left\{\varnothing \right\}\to A=1_{𝑜}$$
18	17	a1d	$$⊢A=\left\{\varnothing \right\}\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)$$
19	14 18	jaoi	$$⊢\left(A=\varnothing \vee A=\left\{\varnothing \right\}\right)\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)$$
20	8 19	sylbi	$$⊢A\subseteq \left\{\varnothing \right\}\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)$$
21	20	a1i	$$⊢\mathrm{Ord}A\to \left(A\subseteq \left\{\varnothing \right\}\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)\right)$$
22		ordtop	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Top}\leftrightarrow A\ne \bigcup A\right)$$
23	22	biimpd	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Top}\to A\ne \bigcup A\right)$$
24	23	necon2bd	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\to \neg A\in \mathrm{Top}\right)$$
25		cmptop	$$⊢A\in \mathrm{Comp}\to A\in \mathrm{Top}$$
26	25	con3i	$$⊢\neg A\in \mathrm{Top}\to \neg A\in \mathrm{Comp}$$
27	24 26	syl6	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\to \neg A\in \mathrm{Comp}\right)$$
28	27	a1dd	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\to \left(\mathrm{Lim}\bigcup A\to \neg A\in \mathrm{Comp}\right)\right)$$
29		limsucncmp	$$⊢\mathrm{Lim}\bigcup A\to \neg \mathrm{suc}\bigcup A\in \mathrm{Comp}$$
30		eleq1	$$⊢A=\mathrm{suc}\bigcup A\to \left(A\in \mathrm{Comp}\leftrightarrow \mathrm{suc}\bigcup A\in \mathrm{Comp}\right)$$
31	30	notbid	$$⊢A=\mathrm{suc}\bigcup A\to \left(\neg A\in \mathrm{Comp}\leftrightarrow \neg \mathrm{suc}\bigcup A\in \mathrm{Comp}\right)$$
32	29 31	syl5ibr	$$⊢A=\mathrm{suc}\bigcup A\to \left(\mathrm{Lim}\bigcup A\to \neg A\in \mathrm{Comp}\right)$$
33	32	a1i	$$⊢\mathrm{Ord}A\to \left(A=\mathrm{suc}\bigcup A\to \left(\mathrm{Lim}\bigcup A\to \neg A\in \mathrm{Comp}\right)\right)$$
34		orduniorsuc	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
35	28 33 34	mpjaod	$$⊢\mathrm{Ord}A\to \left(\mathrm{Lim}\bigcup A\to \neg A\in \mathrm{Comp}\right)$$
36		pm2.21	$$⊢\neg A\in \mathrm{Comp}\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)$$
37	35 36	syl6	$$⊢\mathrm{Ord}A\to \left(\mathrm{Lim}\bigcup A\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)\right)$$
38	21 37	jaod	$$⊢\mathrm{Ord}A\to \left(\left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)\to \left(A\in \mathrm{Comp}\to A=1_{𝑜}\right)\right)$$
39	38	com23	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Comp}\to \left(\left(A\subseteq \left\{\varnothing \right\}\vee \mathrm{Lim}\bigcup A\right)\to A=1_{𝑜}\right)\right)$$
40	7 39	syl5d	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Comp}\to \left(\bigcup A=\bigcup \bigcup A\to A=1_{𝑜}\right)\right)$$
41		ordeleqon	$$⊢\mathrm{Ord}A\leftrightarrow \left(A\in \mathrm{On}\vee A=\mathrm{On}\right)$$
42		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
43	42	eqcomi	$$⊢\mathrm{On}=\bigcup \mathrm{On}$$
44	43	unieqi	$$⊢\bigcup \mathrm{On}=\bigcup \bigcup \mathrm{On}$$
45		unieq	$$⊢A=\mathrm{On}\to \bigcup A=\bigcup \mathrm{On}$$
46	45	unieqd	$$⊢A=\mathrm{On}\to \bigcup \bigcup A=\bigcup \bigcup \mathrm{On}$$
47	44 45 46	3eqtr4a	$$⊢A=\mathrm{On}\to \bigcup A=\bigcup \bigcup A$$
48	47	orim2i	$$⊢\left(A\in \mathrm{On}\vee A=\mathrm{On}\right)\to \left(A\in \mathrm{On}\vee \bigcup A=\bigcup \bigcup A\right)$$
49	41 48	sylbi	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{On}\vee \bigcup A=\bigcup \bigcup A\right)$$
50	49	orcomd	$$⊢\mathrm{Ord}A\to \left(\bigcup A=\bigcup \bigcup A\vee A\in \mathrm{On}\right)$$
51	50	ord	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to A\in \mathrm{On}\right)$$
52		unieq	$$⊢A=\bigcup A\to \bigcup A=\bigcup \bigcup A$$
53	52	con3i	$$⊢\neg \bigcup A=\bigcup \bigcup A\to \neg A=\bigcup A$$
54	34	ord	$$⊢\mathrm{Ord}A\to \left(\neg A=\bigcup A\to A=\mathrm{suc}\bigcup A\right)$$
55	53 54	syl5	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to A=\mathrm{suc}\bigcup A\right)$$
56		orduniorsuc	$$⊢\mathrm{Ord}\bigcup A\to \left(\bigcup A=\bigcup \bigcup A\vee \bigcup A=\mathrm{suc}\bigcup \bigcup A\right)$$
57	1 56	syl	$$⊢\mathrm{Ord}A\to \left(\bigcup A=\bigcup \bigcup A\vee \bigcup A=\mathrm{suc}\bigcup \bigcup A\right)$$
58	57	ord	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to \bigcup A=\mathrm{suc}\bigcup \bigcup A\right)$$
59		suceq	$$⊢\bigcup A=\mathrm{suc}\bigcup \bigcup A\to \mathrm{suc}\bigcup A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A$$
60	58 59	syl6	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to \mathrm{suc}\bigcup A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\right)$$
61		eqtr	$$⊢\left(A=\mathrm{suc}\bigcup A\wedge \mathrm{suc}\bigcup A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\right)\to A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A$$
62	61	ex	$$⊢A=\mathrm{suc}\bigcup A\to \left(\mathrm{suc}\bigcup A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\to A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\right)$$
63	55 60 62	syl6c	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\right)$$
64		onuni	$$⊢A\in \mathrm{On}\to \bigcup A\in \mathrm{On}$$
65		onuni	$$⊢\bigcup A\in \mathrm{On}\to \bigcup \bigcup A\in \mathrm{On}$$
66		onsucsuccmp	$$⊢\bigcup \bigcup A\in \mathrm{On}\to \mathrm{suc}\mathrm{suc}\bigcup \bigcup A\in \mathrm{Comp}$$
67		eleq1a	$$⊢\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\in \mathrm{Comp}\to \left(A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\to A\in \mathrm{Comp}\right)$$
68	64 65 66 67	4syl	$$⊢A\in \mathrm{On}\to \left(A=\mathrm{suc}\mathrm{suc}\bigcup \bigcup A\to A\in \mathrm{Comp}\right)$$
69	51 63 68	syl6c	$$⊢\mathrm{Ord}A\to \left(\neg \bigcup A=\bigcup \bigcup A\to A\in \mathrm{Comp}\right)$$
70		id	$$⊢A=1_{𝑜}\to A=1_{𝑜}$$
71	70 16	eqtrdi	$$⊢A=1_{𝑜}\to A=\left\{\varnothing \right\}$$
72		0cmp	$$⊢\left\{\varnothing \right\}\in \mathrm{Comp}$$
73	71 72	eqeltrdi	$$⊢A=1_{𝑜}\to A\in \mathrm{Comp}$$
74	73	a1i	$$⊢\mathrm{Ord}A\to \left(A=1_{𝑜}\to A\in \mathrm{Comp}\right)$$
75	69 74	jad	$$⊢\mathrm{Ord}A\to \left(\left(\bigcup A=\bigcup \bigcup A\to A=1_{𝑜}\right)\to A\in \mathrm{Comp}\right)$$
76	40 75	impbid	$$⊢\mathrm{Ord}A\to \left(A\in \mathrm{Comp}\leftrightarrow \left(\bigcup A=\bigcup \bigcup A\to A=1_{𝑜}\right)\right)$$