Proof of Theorem ordcmp
Step | Hyp | Ref
| Expression |
1 | | orduni 7530 |
. . . 4
⊢ (Ord
𝐴 → Ord ∪ 𝐴) |
2 | | unizlim 6289 |
. . . . . 6
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (∪ 𝐴 = ∅ ∨ Lim ∪ 𝐴))) |
3 | | uni0b 4824 |
. . . . . . 7
⊢ (∪ 𝐴 =
∅ ↔ 𝐴 ⊆
{∅}) |
4 | 3 | orbi1i 913 |
. . . . . 6
⊢ ((∪ 𝐴 =
∅ ∨ Lim ∪ 𝐴) ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴)) |
5 | 2, 4 | bitrdi 290 |
. . . . 5
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
6 | 5 | biimpd 232 |
. . . 4
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
7 | 1, 6 | syl 17 |
. . 3
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
8 | | sssn 4714 |
. . . . . . 7
⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅})) |
9 | | 0ntop 21658 |
. . . . . . . . . . 11
⊢ ¬
∅ ∈ Top |
10 | | cmptop 22148 |
. . . . . . . . . . 11
⊢ (∅
∈ Comp → ∅ ∈ Top) |
11 | 9, 10 | mto 200 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ Comp |
12 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp ↔ ∅
∈ Comp)) |
13 | 11, 12 | mtbiri 330 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ¬ 𝐴 ∈ Comp) |
14 | 13 | pm2.21d 121 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp → 𝐴 =
1o)) |
15 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 = {∅} → 𝐴 = {∅}) |
16 | | df1o2 8145 |
. . . . . . . . . 10
⊢
1o = {∅} |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝐴 = {∅} → 𝐴 =
1o) |
18 | 17 | a1d 25 |
. . . . . . . 8
⊢ (𝐴 = {∅} → (𝐴 ∈ Comp → 𝐴 =
1o)) |
19 | 14, 18 | jaoi 856 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ∈ Comp → 𝐴 =
1o)) |
20 | 8, 19 | sylbi 220 |
. . . . . 6
⊢ (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 =
1o)) |
21 | 20 | a1i 11 |
. . . . 5
⊢ (Ord
𝐴 → (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 = 1o))) |
22 | | ordtop 34270 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝐴 ∈ Top ↔ 𝐴 ≠ ∪ 𝐴)) |
23 | 22 | biimpd 232 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → (𝐴 ∈ Top → 𝐴 ≠ ∪ 𝐴)) |
24 | 23 | necon2bd 2950 |
. . . . . . . . 9
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Top)) |
25 | | cmptop 22148 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Comp → 𝐴 ∈ Top) |
26 | 25 | con3i 157 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Top → ¬
𝐴 ∈
Comp) |
27 | 24, 26 | syl6 35 |
. . . . . . . 8
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) |
28 | 27 | a1dd 50 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) |
29 | | limsucncmp 34280 |
. . . . . . . . 9
⊢ (Lim
∪ 𝐴 → ¬ suc ∪ 𝐴
∈ Comp) |
30 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝐴 = suc ∪ 𝐴
→ (𝐴 ∈ Comp
↔ suc ∪ 𝐴 ∈ Comp)) |
31 | 30 | notbid 321 |
. . . . . . . . 9
⊢ (𝐴 = suc ∪ 𝐴
→ (¬ 𝐴 ∈ Comp
↔ ¬ suc ∪ 𝐴 ∈ Comp)) |
32 | 29, 31 | syl5ibr 249 |
. . . . . . . 8
⊢ (𝐴 = suc ∪ 𝐴
→ (Lim ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = suc ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) |
34 | | orduniorsuc 7566 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) |
35 | 28, 33, 34 | mpjaod 859 |
. . . . . 6
⊢ (Ord
𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp)) |
36 | | pm2.21 123 |
. . . . . 6
⊢ (¬
𝐴 ∈ Comp → (𝐴 ∈ Comp → 𝐴 =
1o)) |
37 | 35, 36 | syl6 35 |
. . . . 5
⊢ (Ord
𝐴 → (Lim ∪ 𝐴
→ (𝐴 ∈ Comp
→ 𝐴 =
1o))) |
38 | 21, 37 | jaod 858 |
. . . 4
⊢ (Ord
𝐴 → ((𝐴 ⊆ {∅} ∨ Lim
∪ 𝐴) → (𝐴 ∈ Comp → 𝐴 = 1o))) |
39 | 38 | com23 86 |
. . 3
⊢ (Ord
𝐴 → (𝐴 ∈ Comp → ((𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴)
→ 𝐴 =
1o))) |
40 | 7, 39 | syl5d 73 |
. 2
⊢ (Ord
𝐴 → (𝐴 ∈ Comp → (∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1o))) |
41 | | ordeleqon 7524 |
. . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) |
42 | | unon 7567 |
. . . . . . . . . . 11
⊢ ∪ On = On |
43 | 42 | eqcomi 2747 |
. . . . . . . . . 10
⊢ On =
∪ On |
44 | 43 | unieqi 4809 |
. . . . . . . . 9
⊢ ∪ On = ∪ ∪ On |
45 | | unieq 4807 |
. . . . . . . . 9
⊢ (𝐴 = On → ∪ 𝐴 =
∪ On) |
46 | 45 | unieqd 4810 |
. . . . . . . . 9
⊢ (𝐴 = On → ∪ ∪ 𝐴 = ∪ ∪ On) |
47 | 44, 45, 46 | 3eqtr4a 2799 |
. . . . . . . 8
⊢ (𝐴 = On → ∪ 𝐴 =
∪ ∪ 𝐴) |
48 | 47 | orim2i 910 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∨ 𝐴 = On) → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) |
49 | 41, 48 | sylbi 220 |
. . . . . 6
⊢ (Ord
𝐴 → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) |
50 | 49 | orcomd 870 |
. . . . 5
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ 𝐴 ∈ On)) |
51 | 50 | ord 863 |
. . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 ∈ On)) |
52 | | unieq 4807 |
. . . . . . 7
⊢ (𝐴 = ∪
𝐴 → ∪ 𝐴 =
∪ ∪ 𝐴) |
53 | 52 | con3i 157 |
. . . . . 6
⊢ (¬
∪ 𝐴 = ∪ ∪ 𝐴
→ ¬ 𝐴 = ∪ 𝐴) |
54 | 34 | ord 863 |
. . . . . 6
⊢ (Ord
𝐴 → (¬ 𝐴 = ∪
𝐴 → 𝐴 = suc ∪ 𝐴)) |
55 | 53, 54 | syl5 34 |
. . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc ∪ 𝐴)) |
56 | | orduniorsuc 7566 |
. . . . . . . 8
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
57 | 1, 56 | syl 17 |
. . . . . . 7
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
58 | 57 | ord 863 |
. . . . . 6
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
59 | | suceq 6237 |
. . . . . 6
⊢ (∪ 𝐴 =
suc ∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴) |
60 | 58, 59 | syl6 35 |
. . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴)) |
61 | | eqtr 2758 |
. . . . . 6
⊢ ((𝐴 = suc ∪ 𝐴
∧ suc ∪ 𝐴 = suc suc ∪
∪ 𝐴) → 𝐴 = suc suc ∪
∪ 𝐴) |
62 | 61 | ex 416 |
. . . . 5
⊢ (𝐴 = suc ∪ 𝐴
→ (suc ∪ 𝐴 = suc suc ∪
∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) |
63 | 55, 60, 62 | syl6c 70 |
. . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) |
64 | | onuni 7529 |
. . . . 5
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) |
65 | | onuni 7529 |
. . . . 5
⊢ (∪ 𝐴
∈ On → ∪ ∪
𝐴 ∈
On) |
66 | | onsucsuccmp 34278 |
. . . . 5
⊢ (∪ ∪ 𝐴 ∈ On → suc suc ∪ ∪ 𝐴 ∈ Comp) |
67 | | eleq1a 2828 |
. . . . 5
⊢ (suc suc
∪ ∪ 𝐴 ∈ Comp → (𝐴 = suc suc ∪
∪ 𝐴 → 𝐴 ∈ Comp)) |
68 | 64, 65, 66, 67 | 4syl 19 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 = suc suc ∪ ∪ 𝐴 → 𝐴 ∈ Comp)) |
69 | 51, 63, 68 | syl6c 70 |
. . 3
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 ∈ Comp)) |
70 | | id 22 |
. . . . . 6
⊢ (𝐴 = 1o → 𝐴 =
1o) |
71 | 70, 16 | eqtrdi 2789 |
. . . . 5
⊢ (𝐴 = 1o → 𝐴 = {∅}) |
72 | | 0cmp 22147 |
. . . . 5
⊢ {∅}
∈ Comp |
73 | 71, 72 | eqeltrdi 2841 |
. . . 4
⊢ (𝐴 = 1o → 𝐴 ∈ Comp) |
74 | 73 | a1i 11 |
. . 3
⊢ (Ord
𝐴 → (𝐴 = 1o → 𝐴 ∈ Comp)) |
75 | 69, 74 | jad 190 |
. 2
⊢ (Ord
𝐴 → ((∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1o) → 𝐴 ∈ Comp)) |
76 | 40, 75 | impbid 215 |
1
⊢ (Ord
𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1o))) |