Proof of Theorem ordnexbtwnsuc
| Step | Hyp | Ref
| Expression |
| 1 | | ordelord 6406 |
. . . . . 6
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴) |
| 2 | | ordnbtwn 6477 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
| 3 | 2 | pm2.21d 121 |
. . . . . . . . 9
⊢ (Ord
𝐴 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴) → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵))) |
| 4 | 3 | expd 415 |
. . . . . . . 8
⊢ (Ord
𝐴 → (𝐴 ∈ 𝐵 → (𝐵 ∈ suc 𝐴 → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵)))) |
| 5 | 4 | com12 32 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐵 → (Ord 𝐴 → (𝐵 ∈ suc 𝐴 → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵)))) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (Ord 𝐴 → (𝐵 ∈ suc 𝐴 → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵)))) |
| 7 | 1, 6 | mpd 15 |
. . . . 5
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐵 ∈ suc 𝐴 → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵))) |
| 8 | | sucidg 6465 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐴) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ suc 𝐴) |
| 10 | | ordelon 6408 |
. . . . . . . 8
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
| 11 | | onsuc 7831 |
. . . . . . . 8
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → suc 𝐴 ∈ On) |
| 13 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑐 = suc 𝐴 → (𝐴 ∈ 𝑐 ↔ 𝐴 ∈ suc 𝐴)) |
| 14 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑐 = suc 𝐴 → (𝑐 ∈ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) |
| 15 | 13, 14 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑐 = suc 𝐴 → ((𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) ↔ (𝐴 ∈ suc 𝐴 ∧ suc 𝐴 ∈ 𝐵))) |
| 16 | 15 | adantl 481 |
. . . . . . 7
⊢ (((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑐 = suc 𝐴) → ((𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) ↔ (𝐴 ∈ suc 𝐴 ∧ suc 𝐴 ∈ 𝐵))) |
| 17 | 12, 16 | rspcedv 3615 |
. . . . . 6
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → ((𝐴 ∈ suc 𝐴 ∧ suc 𝐴 ∈ 𝐵) → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵))) |
| 18 | 9, 17 | mpand 695 |
. . . . 5
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (suc 𝐴 ∈ 𝐵 → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵))) |
| 19 | 7, 18 | jaod 860 |
. . . 4
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → ((𝐵 ∈ suc 𝐴 ∨ suc 𝐴 ∈ 𝐵) → ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵))) |
| 20 | | ralnex 3072 |
. . . . 5
⊢
(∀𝑐 ∈ On
¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) ↔ ¬ ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵)) |
| 21 | 20 | biimpi 216 |
. . . 4
⊢
(∀𝑐 ∈ On
¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → ¬ ∃𝑐 ∈ On (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵)) |
| 22 | 19, 21 | nsyli 157 |
. . 3
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → ¬ (𝐵 ∈ suc 𝐴 ∨ suc 𝐴 ∈ 𝐵))) |
| 23 | | ordsuci 7828 |
. . . . 5
⊢ (Ord
𝐴 → Ord suc 𝐴) |
| 24 | 1, 23 | syl 17 |
. . . 4
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → Ord suc 𝐴) |
| 25 | | ordtri3 6420 |
. . . 4
⊢ ((Ord
𝐵 ∧ Ord suc 𝐴) → (𝐵 = suc 𝐴 ↔ ¬ (𝐵 ∈ suc 𝐴 ∨ suc 𝐴 ∈ 𝐵))) |
| 26 | 24, 25 | syldan 591 |
. . 3
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐵 = suc 𝐴 ↔ ¬ (𝐵 ∈ suc 𝐴 ∨ suc 𝐴 ∈ 𝐵))) |
| 27 | 22, 26 | sylibrd 259 |
. 2
⊢ ((Ord
𝐵 ∧ 𝐴 ∈ 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → 𝐵 = suc 𝐴)) |
| 28 | 27 | ancoms 458 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → 𝐵 = suc 𝐴)) |