Step | Hyp | Ref
| Expression |
1 | | pw1on 7227 |
. . . . 5
β’ π«
1o β On |
2 | 1 | onsuci 4517 |
. . . 4
β’ suc
π« 1o β On |
3 | | 3on 6430 |
. . . 4
β’
3o β On |
4 | | eleq1 2240 |
. . . . . . . 8
β’ (π₯ = suc π« 1o
β (π₯ β π¦ β suc π«
1o β π¦)) |
5 | | eqeq1 2184 |
. . . . . . . 8
β’ (π₯ = suc π« 1o
β (π₯ = π¦ β suc π«
1o = π¦)) |
6 | | eleq2 2241 |
. . . . . . . 8
β’ (π₯ = suc π« 1o
β (π¦ β π₯ β π¦ β suc π«
1o)) |
7 | 4, 5, 6 | 3orbi123d 1311 |
. . . . . . 7
β’ (π₯ = suc π« 1o
β ((π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β (suc π« 1o β
π¦ β¨ suc π«
1o = π¦ β¨
π¦ β suc π«
1o))) |
8 | 7 | notbid 667 |
. . . . . 6
β’ (π₯ = suc π« 1o
β (Β¬ (π₯ β
π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ (suc π« 1o
β π¦ β¨ suc π«
1o = π¦ β¨
π¦ β suc π«
1o))) |
9 | 8 | notbid 667 |
. . . . 5
β’ (π₯ = suc π« 1o
β (Β¬ Β¬ (π₯
β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ Β¬ (suc π«
1o β π¦ β¨
suc π« 1o = π¦ β¨ π¦ β suc π«
1o))) |
10 | | eleq2 2241 |
. . . . . . . 8
β’ (π¦ = 3o β (suc
π« 1o β π¦ β suc π« 1o β
3o)) |
11 | | eqeq2 2187 |
. . . . . . . 8
β’ (π¦ = 3o β (suc
π« 1o = π¦
β suc π« 1o = 3o)) |
12 | | eleq1 2240 |
. . . . . . . 8
β’ (π¦ = 3o β (π¦ β suc π«
1o β 3o β suc π«
1o)) |
13 | 10, 11, 12 | 3orbi123d 1311 |
. . . . . . 7
β’ (π¦ = 3o β ((suc
π« 1o β π¦ β¨ suc π« 1o = π¦ β¨ π¦ β suc π« 1o) β
(suc π« 1o β 3o β¨ suc π«
1o = 3o β¨ 3o β suc π«
1o))) |
14 | 13 | notbid 667 |
. . . . . 6
β’ (π¦ = 3o β (Β¬
(suc π« 1o β π¦ β¨ suc π« 1o = π¦ β¨ π¦ β suc π« 1o) β
Β¬ (suc π« 1o β 3o β¨ suc π«
1o = 3o β¨ 3o β suc π«
1o))) |
15 | 14 | notbid 667 |
. . . . 5
β’ (π¦ = 3o β (Β¬
Β¬ (suc π« 1o β π¦ β¨ suc π« 1o = π¦ β¨ π¦ β suc π« 1o) β
Β¬ Β¬ (suc π« 1o β 3o β¨ suc
π« 1o = 3o β¨ 3o β suc π«
1o))) |
16 | 9, 15 | rspc2v 2856 |
. . . 4
β’ ((suc
π« 1o β On β§ 3o β On) β
(βπ₯ β On
βπ¦ β On Β¬
Β¬ (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ Β¬ (suc π«
1o β 3o β¨ suc π« 1o =
3o β¨ 3o β suc π«
1o))) |
17 | 2, 3, 16 | mp2an 426 |
. . 3
β’
(βπ₯ β On
βπ¦ β On Β¬
Β¬ (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ Β¬ (suc π«
1o β 3o β¨ suc π« 1o =
3o β¨ 3o β suc π«
1o)) |
18 | | 3ioran 993 |
. . 3
β’ (Β¬
(suc π« 1o β 3o β¨ suc π«
1o = 3o β¨ 3o β suc π«
1o) β (Β¬ suc π« 1o β 3o
β§ Β¬ suc π« 1o = 3o β§ Β¬
3o β suc π« 1o)) |
19 | 17, 18 | sylnib 676 |
. 2
β’
(βπ₯ β On
βπ¦ β On Β¬
Β¬ (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ (Β¬ suc π«
1o β 3o β§ Β¬ suc π« 1o =
3o β§ Β¬ 3o β suc π«
1o)) |
20 | | sucpw1nel3 7234 |
. . . 4
β’ Β¬
suc π« 1o β 3o |
21 | 20 | a1i 9 |
. . 3
β’ (Β¬
EXMID β Β¬ suc π« 1o β
3o) |
22 | | 2on 6428 |
. . . . . . 7
β’
2o β On |
23 | | suc11 4559 |
. . . . . . 7
β’
((π« 1o β On β§ 2o β On)
β (suc π« 1o = suc 2o β π«
1o = 2o)) |
24 | 1, 22, 23 | mp2an 426 |
. . . . . 6
β’ (suc
π« 1o = suc 2o β π« 1o =
2o) |
25 | | df-3o 6421 |
. . . . . . 7
β’
3o = suc 2o |
26 | 25 | eqeq2i 2188 |
. . . . . 6
β’ (suc
π« 1o = 3o β suc π« 1o =
suc 2o) |
27 | | exmidpweq 6911 |
. . . . . 6
β’
(EXMID β π« 1o =
2o) |
28 | 24, 26, 27 | 3bitr4ri 213 |
. . . . 5
β’
(EXMID β suc π« 1o =
3o) |
29 | 28 | notbii 668 |
. . . 4
β’ (Β¬
EXMID β Β¬ suc π« 1o =
3o) |
30 | 29 | biimpi 120 |
. . 3
β’ (Β¬
EXMID β Β¬ suc π« 1o =
3o) |
31 | | 3nelsucpw1 7235 |
. . . 4
β’ Β¬
3o β suc π« 1o |
32 | 31 | a1i 9 |
. . 3
β’ (Β¬
EXMID β Β¬ 3o β suc π«
1o) |
33 | 21, 30, 32 | 3jca 1177 |
. 2
β’ (Β¬
EXMID β (Β¬ suc π« 1o β
3o β§ Β¬ suc π« 1o = 3o β§
Β¬ 3o β suc π« 1o)) |
34 | 19, 33 | nsyl 628 |
1
β’
(βπ₯ β On
βπ¦ β On Β¬
Β¬ (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β Β¬ Β¬
EXMID) |