Proof of Theorem suc11reg
| Step | Hyp | Ref
| Expression |
| 1 | | en2lp 9646 |
. . . . 5
⊢ ¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) |
| 2 | | ianor 984 |
. . . . 5
⊢ (¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) ↔ (¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴)) |
| 3 | 1, 2 | mpbi 230 |
. . . 4
⊢ (¬
𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴) |
| 4 | | sucidg 6465 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) |
| 5 | | eleq2 2830 |
. . . . . . . . . . 11
⊢ (suc
𝐴 = suc 𝐵 → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ suc 𝐵)) |
| 6 | 4, 5 | syl5ibcom 245 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → 𝐴 ∈ suc 𝐵)) |
| 7 | | elsucg 6452 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
| 8 | 6, 7 | sylibd 239 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
| 9 | 8 | imp 406 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ suc 𝐴 = suc 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
| 10 | 9 | ord 865 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐴 ∈ 𝐵 → 𝐴 = 𝐵)) |
| 11 | 10 | ex 412 |
. . . . . 6
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → (¬ 𝐴 ∈ 𝐵 → 𝐴 = 𝐵))) |
| 12 | 11 | com23 86 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ 𝐵 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
| 13 | | sucidg 6465 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → 𝐵 ∈ suc 𝐵) |
| 14 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 = suc 𝐵 → (𝐵 ∈ suc 𝐴 ↔ 𝐵 ∈ suc 𝐵)) |
| 15 | 13, 14 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → 𝐵 ∈ suc 𝐴)) |
| 16 | | elsucg 6452 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))) |
| 17 | 15, 16 | sylibd 239 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))) |
| 18 | 17 | imp 406 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) |
| 19 | 18 | ord 865 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐵 ∈ 𝐴 → 𝐵 = 𝐴)) |
| 20 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
| 21 | 19, 20 | imbitrdi 251 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐵 ∈ 𝐴 → 𝐴 = 𝐵)) |
| 22 | 21 | ex 412 |
. . . . . 6
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → (¬ 𝐵 ∈ 𝐴 → 𝐴 = 𝐵))) |
| 23 | 22 | com23 86 |
. . . . 5
⊢ (𝐵 ∈ V → (¬ 𝐵 ∈ 𝐴 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
| 24 | 12, 23 | jaao 957 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
| 25 | 3, 24 | mpi 20 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
| 26 | | sucexb 7824 |
. . . . 5
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) |
| 27 | | sucexb 7824 |
. . . . . 6
⊢ (𝐵 ∈ V ↔ suc 𝐵 ∈ V) |
| 28 | 27 | notbii 320 |
. . . . 5
⊢ (¬
𝐵 ∈ V ↔ ¬ suc
𝐵 ∈
V) |
| 29 | | nelneq 2865 |
. . . . 5
⊢ ((suc
𝐴 ∈ V ∧ ¬ suc
𝐵 ∈ V) → ¬
suc 𝐴 = suc 𝐵) |
| 30 | 26, 28, 29 | syl2anb 598 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → ¬ suc
𝐴 = suc 𝐵) |
| 31 | 30 | pm2.21d 121 |
. . 3
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
| 32 | | eqcom 2744 |
. . . 4
⊢ (suc
𝐴 = suc 𝐵 ↔ suc 𝐵 = suc 𝐴) |
| 33 | 26 | notbii 320 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ ¬ suc
𝐴 ∈
V) |
| 34 | | nelneq 2865 |
. . . . . . 7
⊢ ((suc
𝐵 ∈ V ∧ ¬ suc
𝐴 ∈ V) → ¬
suc 𝐵 = suc 𝐴) |
| 35 | 27, 33, 34 | syl2anb 598 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ ¬ 𝐴 ∈ V) → ¬ suc
𝐵 = suc 𝐴) |
| 36 | 35 | ancoms 458 |
. . . . 5
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → ¬ suc
𝐵 = suc 𝐴) |
| 37 | 36 | pm2.21d 121 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐵 = suc 𝐴 → 𝐴 = 𝐵)) |
| 38 | 32, 37 | biimtrid 242 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
| 39 | | sucprc 6460 |
. . . . 5
⊢ (¬
𝐴 ∈ V → suc 𝐴 = 𝐴) |
| 40 | | sucprc 6460 |
. . . . 5
⊢ (¬
𝐵 ∈ V → suc 𝐵 = 𝐵) |
| 41 | 39, 40 | eqeqan12d 2751 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ ¬
𝐵 ∈ V) → (suc
𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) |
| 42 | 41 | biimpd 229 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧ ¬
𝐵 ∈ V) → (suc
𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
| 43 | 25, 31, 38, 42 | 4cases 1041 |
. 2
⊢ (suc
𝐴 = suc 𝐵 → 𝐴 = 𝐵) |
| 44 | | suceq 6450 |
. 2
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
| 45 | 43, 44 | impbii 209 |
1
⊢ (suc
𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵) |