Proof of Theorem onomeneqOLD
| Step | Hyp | Ref
| Expression |
| 1 | | php5 9251 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → ¬
𝐵 ≈ suc 𝐵) |
| 2 | 1 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → ¬ 𝐵 ≈ suc 𝐵) |
| 3 | | enen1 9157 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ suc 𝐵 ↔ 𝐵 ≈ suc 𝐵)) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (𝐴 ≈ suc 𝐵 ↔ 𝐵 ≈ suc 𝐵)) |
| 5 | 2, 4 | mtbird 325 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → ¬ 𝐴 ≈ suc 𝐵) |
| 6 | | peano2 7912 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) |
| 7 | | sssucid 6464 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ suc 𝐵 |
| 8 | | ssdomg 9040 |
. . . . . . . . . . . . . 14
⊢ (suc
𝐵 ∈ ω →
(𝐵 ⊆ suc 𝐵 → 𝐵 ≼ suc 𝐵)) |
| 9 | 6, 7, 8 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ω → 𝐵 ≼ suc 𝐵) |
| 10 | | endomtr 9052 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ suc 𝐵) → 𝐴 ≼ suc 𝐵) |
| 11 | 9, 10 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ≼ suc 𝐵) |
| 12 | 11 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → 𝐴 ≼ suc 𝐵) |
| 13 | 12 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ω ∧ 𝐴 ≈ 𝐵) → (ω ⊆ 𝐴 → 𝐴 ≼ suc 𝐵)) |
| 14 | 13 | adantll 714 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (ω ⊆ 𝐴 → 𝐴 ≼ suc 𝐵)) |
| 15 | | ssel 3977 |
. . . . . . . . . . . . . . 15
⊢ (ω
⊆ 𝐴 → (𝐵 ∈ ω → 𝐵 ∈ 𝐴)) |
| 16 | 15 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ω → (ω
⊆ 𝐴 → 𝐵 ∈ 𝐴)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (ω
⊆ 𝐴 → 𝐵 ∈ 𝐴)) |
| 18 | | eloni 6394 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 19 | | ordelsuc 7840 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ω ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ⊆ 𝐴)) |
| 20 | 18, 19 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ⊆ 𝐴)) |
| 21 | 17, 20 | sylibd 239 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (ω
⊆ 𝐴 → suc 𝐵 ⊆ 𝐴)) |
| 22 | | ssdomg 9040 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (suc 𝐵 ⊆ 𝐴 → suc 𝐵 ≼ 𝐴)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (suc 𝐵 ⊆ 𝐴 → suc 𝐵 ≼ 𝐴)) |
| 24 | 21, 23 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ On) → (ω
⊆ 𝐴 → suc 𝐵 ≼ 𝐴)) |
| 25 | 24 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (ω
⊆ 𝐴 → suc 𝐵 ≼ 𝐴)) |
| 26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (ω ⊆ 𝐴 → suc 𝐵 ≼ 𝐴)) |
| 27 | 14, 26 | jcad 512 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (ω ⊆ 𝐴 → (𝐴 ≼ suc 𝐵 ∧ suc 𝐵 ≼ 𝐴))) |
| 28 | | sbth 9133 |
. . . . . . . 8
⊢ ((𝐴 ≼ suc 𝐵 ∧ suc 𝐵 ≼ 𝐴) → 𝐴 ≈ suc 𝐵) |
| 29 | 27, 28 | syl6 35 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (ω ⊆ 𝐴 → 𝐴 ≈ suc 𝐵)) |
| 30 | 5, 29 | mtod 198 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → ¬ ω ⊆ 𝐴) |
| 31 | | ordom 7897 |
. . . . . . . . 9
⊢ Ord
ω |
| 32 | | ordtri1 6417 |
. . . . . . . . 9
⊢ ((Ord
ω ∧ Ord 𝐴) →
(ω ⊆ 𝐴 ↔
¬ 𝐴 ∈
ω)) |
| 33 | 31, 18, 32 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (ω
⊆ 𝐴 ↔ ¬
𝐴 ∈
ω)) |
| 34 | 33 | con2bid 354 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ∈ ω ↔ ¬
ω ⊆ 𝐴)) |
| 35 | 34 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (𝐴 ∈ ω ↔ ¬ ω ⊆
𝐴)) |
| 36 | 30, 35 | mpbird 257 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ ω) |
| 37 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ ω) |
| 38 | 36, 37 | jca 511 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) |
| 39 | | nneneq 9246 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |
| 40 | 39 | biimpa 476 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) |
| 41 | 38, 40 | sylancom 588 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) |
| 42 | 41 | ex 412 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)) |
| 43 | | eqeng 9026 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
| 44 | 43 | adantr 480 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
| 45 | 42, 44 | impbid 212 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |