Metamath Proof Explorer

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 A -> ( A e. Comp <-> ( U. A = U. U. A -> A = 1o ) ) )

Proof

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