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	⊢ ( Ord 𝐴 → ( 𝐴 ∈ Comp ↔ ( ∪ 𝐴 = ∪ ∪ 𝐴 → 𝐴 = 1o ) ) )

Proof

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