Proof of Theorem suc11
Step | Hyp | Ref
| Expression |
1 | | eloni 6228 |
. . . . 5
⊢ (𝐴 ∈ On → Ord 𝐴) |
2 | | ordn2lp 6238 |
. . . . 5
⊢ (Ord
𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)) |
3 | | pm3.13 995 |
. . . . 5
⊢ (¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) → (¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴)) |
4 | 1, 2, 3 | 3syl 18 |
. . . 4
⊢ (𝐴 ∈ On → (¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴)) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴)) |
6 | | eqimss 3962 |
. . . . . 6
⊢ (suc
𝐴 = suc 𝐵 → suc 𝐴 ⊆ suc 𝐵) |
7 | | sucssel 6310 |
. . . . . 6
⊢ (𝐴 ∈ On → (suc 𝐴 ⊆ suc 𝐵 → 𝐴 ∈ suc 𝐵)) |
8 | 6, 7 | syl5 34 |
. . . . 5
⊢ (𝐴 ∈ On → (suc 𝐴 = suc 𝐵 → 𝐴 ∈ suc 𝐵)) |
9 | | elsuci 6284 |
. . . . . . 7
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
10 | 9 | ord 864 |
. . . . . 6
⊢ (𝐴 ∈ suc 𝐵 → (¬ 𝐴 ∈ 𝐵 → 𝐴 = 𝐵)) |
11 | 10 | com12 32 |
. . . . 5
⊢ (¬
𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 → 𝐴 = 𝐵)) |
12 | 8, 11 | syl9 77 |
. . . 4
⊢ (𝐴 ∈ On → (¬ 𝐴 ∈ 𝐵 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
13 | | eqimss2 3963 |
. . . . . 6
⊢ (suc
𝐴 = suc 𝐵 → suc 𝐵 ⊆ suc 𝐴) |
14 | | sucssel 6310 |
. . . . . 6
⊢ (𝐵 ∈ On → (suc 𝐵 ⊆ suc 𝐴 → 𝐵 ∈ suc 𝐴)) |
15 | 13, 14 | syl5 34 |
. . . . 5
⊢ (𝐵 ∈ On → (suc 𝐴 = suc 𝐵 → 𝐵 ∈ suc 𝐴)) |
16 | | elsuci 6284 |
. . . . . . . 8
⊢ (𝐵 ∈ suc 𝐴 → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) |
17 | 16 | ord 864 |
. . . . . . 7
⊢ (𝐵 ∈ suc 𝐴 → (¬ 𝐵 ∈ 𝐴 → 𝐵 = 𝐴)) |
18 | | eqcom 2744 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
19 | 17, 18 | syl6ib 254 |
. . . . . 6
⊢ (𝐵 ∈ suc 𝐴 → (¬ 𝐵 ∈ 𝐴 → 𝐴 = 𝐵)) |
20 | 19 | com12 32 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐴 = 𝐵)) |
21 | 15, 20 | syl9 77 |
. . . 4
⊢ (𝐵 ∈ On → (¬ 𝐵 ∈ 𝐴 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
22 | 12, 21 | jaao 955 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
23 | 5, 22 | mpd 15 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
24 | | suceq 6283 |
. 2
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
25 | 23, 24 | impbid1 228 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) |