Proof of Theorem ordcmp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | orduni 7809 | . . . 4
⊢ (Ord
𝐴 → Ord ∪ 𝐴) | 
| 2 |  | unizlim 6507 | . . . . . 6
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (∪ 𝐴 = ∅ ∨ Lim ∪ 𝐴))) | 
| 3 |  | uni0b 4933 | . . . . . . 7
⊢ (∪ 𝐴 =
∅ ↔ 𝐴 ⊆
{∅}) | 
| 4 | 3 | orbi1i 914 | . . . . . 6
⊢ ((∪ 𝐴 =
∅ ∨ Lim ∪ 𝐴) ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴)) | 
| 5 | 2, 4 | bitrdi 287 | . . . . 5
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ↔ (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) | 
| 6 | 5 | biimpd 229 | . . . 4
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) | 
| 7 | 1, 6 | syl 17 | . . 3
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 → (𝐴 ⊆ {∅} ∨ Lim ∪ 𝐴))) | 
| 8 |  | sssn 4826 | . . . . . . 7
⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅})) | 
| 9 |  | 0ntop 22911 | . . . . . . . . . . 11
⊢  ¬
∅ ∈ Top | 
| 10 |  | cmptop 23403 | . . . . . . . . . . 11
⊢ (∅
∈ Comp → ∅ ∈ Top) | 
| 11 | 9, 10 | mto 197 | . . . . . . . . . 10
⊢  ¬
∅ ∈ Comp | 
| 12 |  | eleq1 2829 | . . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp ↔ ∅
∈ Comp)) | 
| 13 | 11, 12 | mtbiri 327 | . . . . . . . . 9
⊢ (𝐴 = ∅ → ¬ 𝐴 ∈ Comp) | 
| 14 | 13 | pm2.21d 121 | . . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 ∈ Comp → 𝐴 =
1o)) | 
| 15 |  | id 22 | . . . . . . . . . 10
⊢ (𝐴 = {∅} → 𝐴 = {∅}) | 
| 16 |  | df1o2 8513 | . . . . . . . . . 10
⊢
1o = {∅} | 
| 17 | 15, 16 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝐴 = {∅} → 𝐴 =
1o) | 
| 18 | 17 | a1d 25 | . . . . . . . 8
⊢ (𝐴 = {∅} → (𝐴 ∈ Comp → 𝐴 =
1o)) | 
| 19 | 14, 18 | jaoi 858 | . . . . . . 7
⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ∈ Comp → 𝐴 =
1o)) | 
| 20 | 8, 19 | sylbi 217 | . . . . . 6
⊢ (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 =
1o)) | 
| 21 | 20 | a1i 11 | . . . . 5
⊢ (Ord
𝐴 → (𝐴 ⊆ {∅} → (𝐴 ∈ Comp → 𝐴 = 1o))) | 
| 22 |  | ordtop 36437 | . . . . . . . . . . 11
⊢ (Ord
𝐴 → (𝐴 ∈ Top ↔ 𝐴 ≠ ∪ 𝐴)) | 
| 23 | 22 | biimpd 229 | . . . . . . . . . 10
⊢ (Ord
𝐴 → (𝐴 ∈ Top → 𝐴 ≠ ∪ 𝐴)) | 
| 24 | 23 | necon2bd 2956 | . . . . . . . . 9
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Top)) | 
| 25 |  | cmptop 23403 | . . . . . . . . . 10
⊢ (𝐴 ∈ Comp → 𝐴 ∈ Top) | 
| 26 | 25 | con3i 154 | . . . . . . . . 9
⊢ (¬
𝐴 ∈ Top → ¬
𝐴 ∈
Comp) | 
| 27 | 24, 26 | syl6 35 | . . . . . . . 8
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) | 
| 28 | 27 | a1dd 50 | . . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) | 
| 29 |  | limsucncmp 36447 | . . . . . . . . 9
⊢ (Lim
∪ 𝐴 → ¬ suc ∪ 𝐴
∈ Comp) | 
| 30 |  | eleq1 2829 | . . . . . . . . . 10
⊢ (𝐴 = suc ∪ 𝐴
→ (𝐴 ∈ Comp
↔ suc ∪ 𝐴 ∈ Comp)) | 
| 31 | 30 | notbid 318 | . . . . . . . . 9
⊢ (𝐴 = suc ∪ 𝐴
→ (¬ 𝐴 ∈ Comp
↔ ¬ suc ∪ 𝐴 ∈ Comp)) | 
| 32 | 29, 31 | imbitrrid 246 | . . . . . . . 8
⊢ (𝐴 = suc ∪ 𝐴
→ (Lim ∪ 𝐴 → ¬ 𝐴 ∈ Comp)) | 
| 33 | 32 | a1i 11 | . . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = suc ∪ 𝐴 → (Lim ∪ 𝐴
→ ¬ 𝐴 ∈
Comp))) | 
| 34 |  | orduniorsuc 7850 | . . . . . . 7
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) | 
| 35 | 28, 33, 34 | mpjaod 861 | . . . . . 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 860 | . . . 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 7802 | . . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) | 
| 42 |  | unon 7851 | . . . . . . . . . . 11
⊢ ∪ On = On | 
| 43 | 42 | eqcomi 2746 | . . . . . . . . . 10
⊢ On =
∪ On | 
| 44 | 43 | unieqi 4919 | . . . . . . . . 9
⊢ ∪ On = ∪ ∪ On | 
| 45 |  | unieq 4918 | . . . . . . . . 9
⊢ (𝐴 = On → ∪ 𝐴 =
∪ On) | 
| 46 | 45 | unieqd 4920 | . . . . . . . . 9
⊢ (𝐴 = On → ∪ ∪ 𝐴 = ∪ ∪ On) | 
| 47 | 44, 45, 46 | 3eqtr4a 2803 | . . . . . . . 8
⊢ (𝐴 = On → ∪ 𝐴 =
∪ ∪ 𝐴) | 
| 48 | 47 | orim2i 911 | . . . . . . 7
⊢ ((𝐴 ∈ On ∨ 𝐴 = On) → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) | 
| 49 | 41, 48 | sylbi 217 | . . . . . 6
⊢ (Ord
𝐴 → (𝐴 ∈ On ∨ ∪
𝐴 = ∪ ∪ 𝐴)) | 
| 50 | 49 | orcomd 872 | . . . . 5
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ 𝐴 ∈ On)) | 
| 51 | 50 | ord 865 | . . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 ∈ On)) | 
| 52 |  | unieq 4918 | . . . . . . 7
⊢ (𝐴 = ∪
𝐴 → ∪ 𝐴 =
∪ ∪ 𝐴) | 
| 53 | 52 | con3i 154 | . . . . . 6
⊢ (¬
∪ 𝐴 = ∪ ∪ 𝐴
→ ¬ 𝐴 = ∪ 𝐴) | 
| 54 | 34 | ord 865 | . . . . . 6
⊢ (Ord
𝐴 → (¬ 𝐴 = ∪
𝐴 → 𝐴 = suc ∪ 𝐴)) | 
| 55 | 53, 54 | syl5 34 | . . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc ∪ 𝐴)) | 
| 56 |  | orduniorsuc 7850 | . . . . . . . 8
⊢ (Ord
∪ 𝐴 → (∪ 𝐴 = ∪
∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) | 
| 57 | 1, 56 | syl 17 | . . . . . . 7
⊢ (Ord
𝐴 → (∪ 𝐴 =
∪ ∪ 𝐴 ∨ ∪ 𝐴 = suc ∪ ∪ 𝐴)) | 
| 58 | 57 | ord 865 | . . . . . 6
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → ∪ 𝐴 = suc ∪ ∪ 𝐴)) | 
| 59 |  | suceq 6450 | . . . . . 6
⊢ (∪ 𝐴 =
suc ∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴) | 
| 60 | 58, 59 | syl6 35 | . . . . 5
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → suc ∪
𝐴 = suc suc ∪ ∪ 𝐴)) | 
| 61 |  | eqtr 2760 | . . . . . 6
⊢ ((𝐴 = suc ∪ 𝐴
∧ suc ∪ 𝐴 = suc suc ∪
∪ 𝐴) → 𝐴 = suc suc ∪
∪ 𝐴) | 
| 62 | 61 | ex 412 | . . . . 5
⊢ (𝐴 = suc ∪ 𝐴
→ (suc ∪ 𝐴 = suc suc ∪
∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) | 
| 63 | 55, 60, 62 | syl6c 70 | . . . 4
⊢ (Ord
𝐴 → (¬ ∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = suc suc ∪
∪ 𝐴)) | 
| 64 |  | onuni 7808 | . . . . 5
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) | 
| 65 |  | onuni 7808 | . . . . 5
⊢ (∪ 𝐴
∈ On → ∪ ∪
𝐴 ∈
On) | 
| 66 |  | onsucsuccmp 36445 | . . . . 5
⊢ (∪ ∪ 𝐴 ∈ On → suc suc ∪ ∪ 𝐴 ∈ Comp) | 
| 67 |  | eleq1a 2836 | . . . . 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 2793 | . . . . 5
⊢ (𝐴 = 1o → 𝐴 = {∅}) | 
| 72 |  | 0cmp 23402 | . . . . 5
⊢ {∅}
∈ Comp | 
| 73 | 71, 72 | eqeltrdi 2849 | . . . 4
⊢ (𝐴 = 1o → 𝐴 ∈ Comp) | 
| 74 | 73 | a1i 11 | . . 3
⊢ (Ord
𝐴 → (𝐴 = 1o → 𝐴 ∈ Comp)) | 
| 75 | 69, 74 | jad 187 | . 2
⊢ (Ord
𝐴 → ((∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1o) → 𝐴 ∈ Comp)) | 
| 76 | 40, 75 | impbid 212 | 1
⊢ (Ord
𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 =
∪ ∪ 𝐴 → 𝐴 = 1o))) |