Proof of Theorem suc11g
Step | Hyp | Ref
| Expression |
1 | | en2lp 4232 |
. . . 4
⊢ ¬
(B ∈
A ∧
A ∈
B) |
2 | | sucidg 4119 |
. . . . . . . . . . . 12
⊢ (B ∈ 𝑊 → B ∈ suc B) |
3 | | eleq2 2098 |
. . . . . . . . . . . 12
⊢ (suc
A = suc B → (B
∈ suc A
↔ B ∈ suc B)) |
4 | 2, 3 | syl5ibrcom 146 |
. . . . . . . . . . 11
⊢ (B ∈ 𝑊 → (suc A = suc B →
B ∈ suc
A)) |
5 | | elsucg 4107 |
. . . . . . . . . . 11
⊢ (B ∈ 𝑊 → (B ∈ suc A ↔ (B
∈ A ∨ B = A))) |
6 | 4, 5 | sylibd 138 |
. . . . . . . . . 10
⊢ (B ∈ 𝑊 → (suc A = suc B →
(B ∈
A ∨
B = A))) |
7 | 6 | imp 115 |
. . . . . . . . 9
⊢
((B ∈ 𝑊 ∧ suc
A = suc B) → (B
∈ A ∨ B = A)) |
8 | 7 | 3adant1 921 |
. . . . . . . 8
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → (B ∈ A ∨ B = A)) |
9 | | sucidg 4119 |
. . . . . . . . . . . 12
⊢ (A ∈ 𝑉 → A ∈ suc A) |
10 | | eleq2 2098 |
. . . . . . . . . . . 12
⊢ (suc
A = suc B → (A
∈ suc A
↔ A ∈ suc B)) |
11 | 9, 10 | syl5ibcom 144 |
. . . . . . . . . . 11
⊢ (A ∈ 𝑉 → (suc A = suc B →
A ∈ suc
B)) |
12 | | elsucg 4107 |
. . . . . . . . . . 11
⊢ (A ∈ 𝑉 → (A ∈ suc B ↔ (A
∈ B ∨ A = B))) |
13 | 11, 12 | sylibd 138 |
. . . . . . . . . 10
⊢ (A ∈ 𝑉 → (suc A = suc B →
(A ∈
B ∨
A = B))) |
14 | 13 | imp 115 |
. . . . . . . . 9
⊢
((A ∈ 𝑉 ∧ suc
A = suc B) → (A
∈ B ∨ A = B)) |
15 | 14 | 3adant2 922 |
. . . . . . . 8
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → (A ∈ B ∨ A = B)) |
16 | 8, 15 | jca 290 |
. . . . . . 7
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → ((B ∈ A ∨ B = A) ∧ (A ∈ B ∨ A = B))) |
17 | | eqcom 2039 |
. . . . . . . . 9
⊢ (B = A ↔
A = B) |
18 | 17 | orbi2i 678 |
. . . . . . . 8
⊢
((B ∈ A ∨ B = A) ↔ (B
∈ A ∨ A = B)) |
19 | 18 | anbi1i 431 |
. . . . . . 7
⊢
(((B ∈ A ∨ B = A) ∧ (A ∈ B ∨ A = B)) ↔
((B ∈
A ∨
A = B)
∧ (A ∈ B ∨ A = B))) |
20 | 16, 19 | sylib 127 |
. . . . . 6
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → ((B ∈ A ∨ A = B) ∧ (A ∈ B ∨ A = B))) |
21 | | ordir 729 |
. . . . . 6
⊢
(((B ∈ A ∧ A ∈ B) ∨ A = B) ↔ ((B
∈ A ∨ A = B) ∧ (A ∈ B ∨ A = B))) |
22 | 20, 21 | sylibr 137 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → ((B ∈ A ∧ A ∈ B) ∨ A = B)) |
23 | 22 | ord 642 |
. . . 4
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → (¬ (B ∈ A ∧ A ∈ B) → A =
B)) |
24 | 1, 23 | mpi 15 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ suc A = suc
B) → A = B) |
25 | 24 | 3expia 1105 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (suc A = suc B →
A = B)) |
26 | | suceq 4105 |
. 2
⊢ (A = B → suc
A = suc B) |
27 | 25, 26 | impbid1 130 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (suc A = suc B ↔
A = B)) |