Step | Hyp | Ref
| Expression |
1 | | eloni 6375 |
. . 3
β’ (π΄ β On β Ord π΄) |
2 | | df-ral 3063 |
. . . . . 6
β’
(βπ β
suc π΄(π₯ β π β π¦ β π) β βπ(π β suc π΄ β (π₯ β π β π¦ β π))) |
3 | | ordelon 6389 |
. . . . . . . . . . 11
β’ ((Ord
π΄ β§ π₯ β π΄) β π₯ β On) |
4 | | ordelon 6389 |
. . . . . . . . . . 11
β’ ((Ord
π΄ β§ π¦ β π΄) β π¦ β On) |
5 | 3, 4 | anim12dan 620 |
. . . . . . . . . 10
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯ β On β§ π¦ β On)) |
6 | | ordsuc 7801 |
. . . . . . . . . . . 12
β’ (Ord
π΄ β Ord suc π΄) |
7 | | ordelon 6389 |
. . . . . . . . . . . . 13
β’ ((Ord suc
π΄ β§ π β suc π΄) β π β On) |
8 | 7 | ex 414 |
. . . . . . . . . . . 12
β’ (Ord suc
π΄ β (π β suc π΄ β π β On)) |
9 | 6, 8 | sylbi 216 |
. . . . . . . . . . 11
β’ (Ord
π΄ β (π β suc π΄ β π β On)) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (π β suc π΄ β π β On)) |
11 | | notbi 319 |
. . . . . . . . . . . 12
β’ ((π₯ β π β π¦ β π) β (Β¬ π₯ β π β Β¬ π¦ β π)) |
12 | | ontri1 6399 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ π₯ β On) β (π β π₯ β Β¬ π₯ β π)) |
13 | | onsssuc 6455 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ π₯ β On) β (π β π₯ β π β suc π₯)) |
14 | 12, 13 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ ((π β On β§ π₯ β On) β (Β¬ π₯ β π β π β suc π₯)) |
15 | 14 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β On β§ (π₯ β On β§ π¦ β On)) β (Β¬ π₯ β π β π β suc π₯)) |
16 | | ontri1 6399 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ π¦ β On) β (π β π¦ β Β¬ π¦ β π)) |
17 | | onsssuc 6455 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ π¦ β On) β (π β π¦ β π β suc π¦)) |
18 | 16, 17 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ ((π β On β§ π¦ β On) β (Β¬ π¦ β π β π β suc π¦)) |
19 | 18 | adantrl 715 |
. . . . . . . . . . . . . 14
β’ ((π β On β§ (π₯ β On β§ π¦ β On)) β (Β¬ π¦ β π β π β suc π¦)) |
20 | 15, 19 | bibi12d 346 |
. . . . . . . . . . . . 13
β’ ((π β On β§ (π₯ β On β§ π¦ β On)) β ((Β¬
π₯ β π β Β¬ π¦ β π) β (π β suc π₯ β π β suc π¦))) |
21 | 20 | ancoms 460 |
. . . . . . . . . . . 12
β’ (((π₯ β On β§ π¦ β On) β§ π β On) β ((Β¬ π₯ β π β Β¬ π¦ β π) β (π β suc π₯ β π β suc π¦))) |
22 | 11, 21 | bitrid 283 |
. . . . . . . . . . 11
β’ (((π₯ β On β§ π¦ β On) β§ π β On) β ((π₯ β π β π¦ β π) β (π β suc π₯ β π β suc π¦))) |
23 | 22 | biimpd 228 |
. . . . . . . . . 10
β’ (((π₯ β On β§ π¦ β On) β§ π β On) β ((π₯ β π β π¦ β π) β (π β suc π₯ β π β suc π¦))) |
24 | 5, 10, 23 | syl6an 683 |
. . . . . . . . 9
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (π β suc π΄ β ((π₯ β π β π¦ β π) β (π β suc π₯ β π β suc π¦)))) |
25 | 24 | a2d 29 |
. . . . . . . 8
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π β suc π΄ β (π₯ β π β π¦ β π)) β (π β suc π΄ β (π β suc π₯ β π β suc π¦)))) |
26 | | ordelss 6381 |
. . . . . . . . . . . . . 14
β’ ((Ord
π΄ β§ π₯ β π΄) β π₯ β π΄) |
27 | | ordelord 6387 |
. . . . . . . . . . . . . . 15
β’ ((Ord
π΄ β§ π₯ β π΄) β Ord π₯) |
28 | | ordsucsssuc 7811 |
. . . . . . . . . . . . . . . 16
β’ ((Ord
π₯ β§ Ord π΄) β (π₯ β π΄ β suc π₯ β suc π΄)) |
29 | 28 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((Ord
π΄ β§ Ord π₯) β (π₯ β π΄ β suc π₯ β suc π΄)) |
30 | 27, 29 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((Ord
π΄ β§ π₯ β π΄) β (π₯ β π΄ β suc π₯ β suc π΄)) |
31 | 26, 30 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((Ord
π΄ β§ π₯ β π΄) β suc π₯ β suc π΄) |
32 | 31 | ssneld 3985 |
. . . . . . . . . . . 12
β’ ((Ord
π΄ β§ π₯ β π΄) β (Β¬ π β suc π΄ β Β¬ π β suc π₯)) |
33 | 32 | adantrr 716 |
. . . . . . . . . . 11
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (Β¬ π β suc π΄ β Β¬ π β suc π₯)) |
34 | | ordelss 6381 |
. . . . . . . . . . . . . 14
β’ ((Ord
π΄ β§ π¦ β π΄) β π¦ β π΄) |
35 | | ordelord 6387 |
. . . . . . . . . . . . . . 15
β’ ((Ord
π΄ β§ π¦ β π΄) β Ord π¦) |
36 | | ordsucsssuc 7811 |
. . . . . . . . . . . . . . . 16
β’ ((Ord
π¦ β§ Ord π΄) β (π¦ β π΄ β suc π¦ β suc π΄)) |
37 | 36 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((Ord
π΄ β§ Ord π¦) β (π¦ β π΄ β suc π¦ β suc π΄)) |
38 | 35, 37 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((Ord
π΄ β§ π¦ β π΄) β (π¦ β π΄ β suc π¦ β suc π΄)) |
39 | 34, 38 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((Ord
π΄ β§ π¦ β π΄) β suc π¦ β suc π΄) |
40 | 39 | ssneld 3985 |
. . . . . . . . . . . 12
β’ ((Ord
π΄ β§ π¦ β π΄) β (Β¬ π β suc π΄ β Β¬ π β suc π¦)) |
41 | 40 | adantrl 715 |
. . . . . . . . . . 11
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (Β¬ π β suc π΄ β Β¬ π β suc π¦)) |
42 | 33, 41 | jcad 514 |
. . . . . . . . . 10
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (Β¬ π β suc π΄ β (Β¬ π β suc π₯ β§ Β¬ π β suc π¦))) |
43 | | pm5.21 824 |
. . . . . . . . . 10
β’ ((Β¬
π β suc π₯ β§ Β¬ π β suc π¦) β (π β suc π₯ β π β suc π¦)) |
44 | 42, 43 | syl6 35 |
. . . . . . . . 9
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (Β¬ π β suc π΄ β (π β suc π₯ β π β suc π¦))) |
45 | | idd 24 |
. . . . . . . . 9
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π β suc π₯ β π β suc π¦) β (π β suc π₯ β π β suc π¦))) |
46 | 44, 45 | jad 187 |
. . . . . . . 8
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π β suc π΄ β (π β suc π₯ β π β suc π¦)) β (π β suc π₯ β π β suc π¦))) |
47 | 25, 46 | syld 47 |
. . . . . . 7
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π β suc π΄ β (π₯ β π β π¦ β π)) β (π β suc π₯ β π β suc π¦))) |
48 | 47 | alimdv 1920 |
. . . . . 6
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ(π β suc π΄ β (π₯ β π β π¦ β π)) β βπ(π β suc π₯ β π β suc π¦))) |
49 | 2, 48 | biimtrid 241 |
. . . . 5
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ β suc π΄(π₯ β π β π¦ β π) β βπ(π β suc π₯ β π β suc π¦))) |
50 | | dfcleq 2726 |
. . . . . . 7
β’ (suc
π₯ = suc π¦ β βπ(π β suc π₯ β π β suc π¦)) |
51 | | suc11 6472 |
. . . . . . 7
β’ ((π₯ β On β§ π¦ β On) β (suc π₯ = suc π¦ β π₯ = π¦)) |
52 | 50, 51 | bitr3id 285 |
. . . . . 6
β’ ((π₯ β On β§ π¦ β On) β
(βπ(π β suc π₯ β π β suc π¦) β π₯ = π¦)) |
53 | 5, 52 | syl 17 |
. . . . 5
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ(π β suc π₯ β π β suc π¦) β π₯ = π¦)) |
54 | 49, 53 | sylibd 238 |
. . . 4
β’ ((Ord
π΄ β§ (π₯ β π΄ β§ π¦ β π΄)) β (βπ β suc π΄(π₯ β π β π¦ β π) β π₯ = π¦)) |
55 | 54 | ralrimivva 3201 |
. . 3
β’ (Ord
π΄ β βπ₯ β π΄ βπ¦ β π΄ (βπ β suc π΄(π₯ β π β π¦ β π) β π₯ = π¦)) |
56 | 1, 55 | syl 17 |
. 2
β’ (π΄ β On β βπ₯ β π΄ βπ¦ β π΄ (βπ β suc π΄(π₯ β π β π¦ β π) β π₯ = π¦)) |
57 | | onsuctopon 35319 |
. . 3
β’ (π΄ β On β suc π΄ β (TopOnβπ΄)) |
58 | | ist0-2 22848 |
. . 3
β’ (suc
π΄ β (TopOnβπ΄) β (suc π΄ β Kol2 β βπ₯ β π΄ βπ¦ β π΄ (βπ β suc π΄(π₯ β π β π¦ β π) β π₯ = π¦))) |
59 | 57, 58 | syl 17 |
. 2
β’ (π΄ β On β (suc π΄ β Kol2 β
βπ₯ β π΄ βπ¦ β π΄ (βπ β suc π΄(π₯ β π β π¦ β π) β π₯ = π¦))) |
60 | 56, 59 | mpbird 257 |
1
β’ (π΄ β On β suc π΄ β Kol2) |