Proof of Theorem suc11reg
Step | Hyp | Ref
| Expression |
1 | | en2lp 9142 |
. . . . 5
⊢ ¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) |
2 | | ianor 981 |
. . . . 5
⊢ (¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) ↔ (¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴)) |
3 | 1, 2 | mpbi 233 |
. . . 4
⊢ (¬
𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴) |
4 | | sucidg 6250 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) |
5 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (suc
𝐴 = suc 𝐵 → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ suc 𝐵)) |
6 | 4, 5 | syl5ibcom 248 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → 𝐴 ∈ suc 𝐵)) |
7 | | elsucg 6239 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
8 | 6, 7 | sylibd 242 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
9 | 8 | imp 410 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ suc 𝐴 = suc 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
10 | 9 | ord 863 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐴 ∈ 𝐵 → 𝐴 = 𝐵)) |
11 | 10 | ex 416 |
. . . . . 6
⊢ (𝐴 ∈ V → (suc 𝐴 = suc 𝐵 → (¬ 𝐴 ∈ 𝐵 → 𝐴 = 𝐵))) |
12 | 11 | com23 86 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ 𝐵 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
13 | | sucidg 6250 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → 𝐵 ∈ suc 𝐵) |
14 | | eleq2 2821 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 = suc 𝐵 → (𝐵 ∈ suc 𝐴 ↔ 𝐵 ∈ suc 𝐵)) |
15 | 13, 14 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → 𝐵 ∈ suc 𝐴)) |
16 | | elsucg 6239 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))) |
17 | 15, 16 | sylibd 242 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))) |
18 | 17 | imp 410 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴)) |
19 | 18 | ord 863 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐵 ∈ 𝐴 → 𝐵 = 𝐴)) |
20 | | eqcom 2745 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
21 | 19, 20 | syl6ib 254 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ suc 𝐴 = suc 𝐵) → (¬ 𝐵 ∈ 𝐴 → 𝐴 = 𝐵)) |
22 | 21 | ex 416 |
. . . . . 6
⊢ (𝐵 ∈ V → (suc 𝐴 = suc 𝐵 → (¬ 𝐵 ∈ 𝐴 → 𝐴 = 𝐵))) |
23 | 22 | com23 86 |
. . . . 5
⊢ (𝐵 ∈ V → (¬ 𝐵 ∈ 𝐴 → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
24 | 12, 23 | jaao 954 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((¬ 𝐴 ∈ 𝐵 ∨ ¬ 𝐵 ∈ 𝐴) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵))) |
25 | 3, 24 | mpi 20 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
26 | | sucexb 7543 |
. . . . 5
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) |
27 | | sucexb 7543 |
. . . . . 6
⊢ (𝐵 ∈ V ↔ suc 𝐵 ∈ V) |
28 | 27 | notbii 323 |
. . . . 5
⊢ (¬
𝐵 ∈ V ↔ ¬ suc
𝐵 ∈
V) |
29 | | nelneq 2857 |
. . . . 5
⊢ ((suc
𝐴 ∈ V ∧ ¬ suc
𝐵 ∈ V) → ¬
suc 𝐴 = suc 𝐵) |
30 | 26, 28, 29 | syl2anb 601 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → ¬ suc
𝐴 = suc 𝐵) |
31 | 30 | pm2.21d 121 |
. . 3
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
32 | | eqcom 2745 |
. . . 4
⊢ (suc
𝐴 = suc 𝐵 ↔ suc 𝐵 = suc 𝐴) |
33 | 26 | notbii 323 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ ¬ suc
𝐴 ∈
V) |
34 | | nelneq 2857 |
. . . . . . 7
⊢ ((suc
𝐵 ∈ V ∧ ¬ suc
𝐴 ∈ V) → ¬
suc 𝐵 = suc 𝐴) |
35 | 27, 33, 34 | syl2anb 601 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ ¬ 𝐴 ∈ V) → ¬ suc
𝐵 = suc 𝐴) |
36 | 35 | ancoms 462 |
. . . . 5
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → ¬ suc
𝐵 = suc 𝐴) |
37 | 36 | pm2.21d 121 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐵 = suc 𝐴 → 𝐴 = 𝐵)) |
38 | 32, 37 | syl5bi 245 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧ 𝐵 ∈ V) → (suc 𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
39 | | sucprc 6247 |
. . . . 5
⊢ (¬
𝐴 ∈ V → suc 𝐴 = 𝐴) |
40 | | sucprc 6247 |
. . . . 5
⊢ (¬
𝐵 ∈ V → suc 𝐵 = 𝐵) |
41 | 39, 40 | eqeqan12d 2755 |
. . . 4
⊢ ((¬
𝐴 ∈ V ∧ ¬
𝐵 ∈ V) → (suc
𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) |
42 | 41 | biimpd 232 |
. . 3
⊢ ((¬
𝐴 ∈ V ∧ ¬
𝐵 ∈ V) → (suc
𝐴 = suc 𝐵 → 𝐴 = 𝐵)) |
43 | 25, 31, 38, 42 | 4cases 1040 |
. 2
⊢ (suc
𝐴 = suc 𝐵 → 𝐴 = 𝐵) |
44 | | suceq 6237 |
. 2
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵) |
45 | 43, 44 | impbii 212 |
1
⊢ (suc
𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵) |