Proof of Theorem ordcmp
Step | Hyp | Ref
| Expression |
1 | | orduni 7036 |
. . . 4
⊢ (Ord
𝐴 → Ord ∪ 𝐴) |
2 | | unizlim 5882 |
. . . . . 6
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (∪ 𝐴 = ∅ ∨ Lim ∪ 𝐴))) |
3 | | uni0b 4495 |
. . . . . . 7
⊢ (∪ 𝐴 =
∅ ↔ 𝐴 ⊆
{∅}) |
4 | 3 | orbi1i 541 |
. . . . . 6
⊢ ((∪ 𝐴 =
∅ ∨ Lim ∪ 𝐴) ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴)) |
5 | 2, 4 | syl6bb 276 |
. . . . 5
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
6 | 5 | biimpd 219 |
. . . 4
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
7 | 1, 6 | syl 17 |
. . 3
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) |
8 | | sssn 4390 |
. . . . . . 7
⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅})) |
9 | | 0ntop 20758 |
. . . . . . . . . . 11
⊢ ¬
∅ ∈ Top |
10 | | cmptop 21246 |
. . . . . . . . . . 11
⊢ (∅
∈ Comp → ∅ ∈ Top) |
11 | 9, 10 | mto 188 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ Comp |
12 | | eleq1 2718 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp ↔ ∅
∈ Comp)) |
13 | 11, 12 | mtbiri 316 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ¬ 𝐴 ∈ Comp) |
14 | 13 | pm2.21d 118 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp → 𝐴 =
1𝑜)) |
15 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 = {∅} → 𝐴 = {∅}) |
16 | | df1o2 7617 |
. . . . . . . . . 10
⊢
1𝑜 = {∅} |
17 | 15, 16 | syl6eqr 2703 |
. . . . . . . . 9
⊢ (𝐴 = {∅} → 𝐴 =
1𝑜) |
18 | 17 | a1d 25 |
. . . . . . . 8
⊢ (𝐴 = {∅} → (𝐴 ∈ Comp → 𝐴 =
1𝑜)) |
19 | 14, 18 | jaoi 393 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ∈ Comp → 𝐴 =
1𝑜)) |
20 | 8, 19 | sylbi 207 |
. . . . . 6
⊢ (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 =
1𝑜)) |
21 | 20 | a1i 11 |
. . . . 5
⊢ (Ord
𝐴 → (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 = 1𝑜))) |
22 | | ordtop 32560 |
. . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝐴 ∈ Top ↔ 𝐴 ≠ ∪ 𝐴)) |
23 | 22 | biimpd 219 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → (𝐴 ∈ Top → 𝐴 ≠ ∪ 𝐴)) |
24 | 23 | necon2bd 2839 |
. . . . . . . . 9
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Top)) |
25 | | cmptop 21246 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Comp → 𝐴 ∈ Top) |
26 | 25 | con3i 150 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Top → ¬
𝐴 ∈
Comp) |
27 | 24, 26 | syl6 35 |
. . . . . . . 8
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) |
28 | 27 | a1dd 50 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) |
29 | | limsucncmp 32570 |
. . . . . . . . 9
⊢ (Lim
∪ 𝐴 → ¬ suc ∪ 𝐴
∈ Comp) |
30 | | eleq1 2718 |
. . . . . . . . . 10
⊢ (𝐴 = suc ∪ 𝐴
→ (𝐴 ∈ Comp
↔ suc ∪ 𝐴 ∈ Comp)) |
31 | 30 | notbid 307 |
. . . . . . . . 9
⊢ (𝐴 = suc ∪ 𝐴
→ (¬ 𝐴 ∈ Comp
↔ ¬ suc ∪ 𝐴 ∈ Comp)) |
32 | 29, 31 | syl5ibr 236 |
. . . . . . . 8
⊢ (𝐴 = suc ∪ 𝐴
→ (Lim ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = suc ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) |
34 | | orduniorsuc 7072 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) |
35 | 28, 33, 34 | mpjaod 395 |
. . . . . 6
⊢ (Ord
𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp)) |
36 | | pm2.21 120 |
. . . . . 6
⊢ (¬
𝐴 ∈ Comp → (𝐴 ∈ Comp → 𝐴 =
1𝑜)) |
37 | 35, 36 | syl6 35 |
. . . . 5
⊢ (Ord
𝐴 → (Lim ∪ 𝐴
→ (𝐴 ∈ Comp
→ 𝐴 =
1𝑜))) |
38 | 21, 37 | jaod 394 |
. . . 4
⊢ (Ord
𝐴 → ((𝐴 ⊆ {∅} ∨ Lim
∪ 𝐴) → (𝐴 ∈ Comp → 𝐴 = 1𝑜))) |
39 | 38 | com23 86 |
. . 3
⊢ (Ord
𝐴 → (𝐴 ∈ Comp → ((𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴)
→ 𝐴 =
1𝑜))) |
40 | 7, 39 | syl5d 73 |
. 2
⊢ (Ord
𝐴 → (𝐴 ∈ Comp → (∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1𝑜))) |
41 | | ordeleqon 7030 |
. . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) |
42 | | unon 7073 |
. . . . . . . . . . 11
⊢ ∪ On = On |
43 | 42 | eqcomi 2660 |
. . . . . . . . . 10
⊢ On =
∪ On |
44 | 43 | unieqi 4477 |
. . . . . . . . 9
⊢ ∪ On = ∪ ∪ On |
45 | | unieq 4476 |
. . . . . . . . 9
⊢ (𝐴 = On → ∪ 𝐴 =
∪ On) |
46 | 45 | unieqd 4478 |
. . . . . . . . 9
⊢ (𝐴 = On → ∪ ∪ 𝐴 = ∪ ∪ On) |
47 | 44, 45, 46 | 3eqtr4a 2711 |
. . . . . . . 8
⊢ (𝐴 = On → ∪ 𝐴 =
∪ ∪ 𝐴) |
48 | 47 | orim2i 539 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∨ 𝐴 = On) → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) |
49 | 41, 48 | sylbi 207 |
. . . . . 6
⊢ (Ord
𝐴 → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) |
50 | 49 | orcomd 402 |
. . . . 5
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ 𝐴 ∈ On)) |
51 | 50 | ord 391 |
. . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 ∈ On)) |
52 | | unieq 4476 |
. . . . . . 7
⊢ (𝐴 = ∪
𝐴 → ∪ 𝐴 =
∪ ∪ 𝐴) |
53 | 52 | con3i 150 |
. . . . . 6
⊢ (¬
∪ 𝐴 = ∪ ∪ 𝐴
→ ¬ 𝐴 = ∪ 𝐴) |
54 | 34 | ord 391 |
. . . . . 6
⊢ (Ord
𝐴 → (¬ 𝐴 = ∪
𝐴 → 𝐴 = suc ∪ 𝐴)) |
55 | 53, 54 | syl5 34 |
. . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc ∪ 𝐴)) |
56 | | orduniorsuc 7072 |
. . . . . . . 8
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
57 | 1, 56 | syl 17 |
. . . . . . 7
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
58 | 57 | ord 391 |
. . . . . 6
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → ∪ 𝐴 = suc ∪ ∪ 𝐴)) |
59 | | suceq 5828 |
. . . . . 6
⊢ (∪ 𝐴 =
suc ∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴) |
60 | 58, 59 | syl6 35 |
. . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴)) |
61 | | eqtr 2670 |
. . . . . 6
⊢ ((𝐴 = suc ∪ 𝐴
∧ suc ∪ 𝐴 = suc suc ∪
∪ 𝐴) → 𝐴 = suc suc ∪
∪ 𝐴) |
62 | 61 | ex 449 |
. . . . 5
⊢ (𝐴 = suc ∪ 𝐴
→ (suc ∪ 𝐴 = suc suc ∪
∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) |
63 | 55, 60, 62 | syl6c 70 |
. . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) |
64 | | onuni 7035 |
. . . . 5
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) |
65 | | onuni 7035 |
. . . . 5
⊢ (∪ 𝐴
∈ On → ∪ ∪
𝐴 ∈
On) |
66 | | onsucsuccmp 32568 |
. . . . 5
⊢ (∪ ∪ 𝐴 ∈ On → suc suc ∪ ∪ 𝐴 ∈ Comp) |
67 | | eleq1a 2725 |
. . . . 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
⊢ (𝐴 = 1𝑜 →
𝐴 =
1𝑜) |
71 | 70, 16 | syl6eq 2701 |
. . . . 5
⊢ (𝐴 = 1𝑜 →
𝐴 =
{∅}) |
72 | | 0cmp 21245 |
. . . . 5
⊢ {∅}
∈ Comp |
73 | 71, 72 | syl6eqel 2738 |
. . . 4
⊢ (𝐴 = 1𝑜 →
𝐴 ∈
Comp) |
74 | 73 | a1i 11 |
. . 3
⊢ (Ord
𝐴 → (𝐴 = 1𝑜 → 𝐴 ∈ Comp)) |
75 | 69, 74 | jad 174 |
. 2
⊢ (Ord
𝐴 → ((∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1𝑜) → 𝐴 ∈ Comp)) |
76 | 40, 75 | impbid 202 |
1
⊢ (Ord
𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1𝑜))) |