Step | Hyp | Ref
| Expression |
1 | | r1fnon 9762 |
. . 3
β’
π
1 Fn On |
2 | | dffn2 6720 |
. . 3
β’
(π
1 Fn On β
π
1:OnβΆV) |
3 | 1, 2 | mpbi 229 |
. 2
β’
π
1:OnβΆV |
4 | | eloni 6375 |
. . . . 5
β’ (π₯ β On β Ord π₯) |
5 | | eloni 6375 |
. . . . 5
β’ (π¦ β On β Ord π¦) |
6 | | ordtri3or 6397 |
. . . . 5
β’ ((Ord
π₯ β§ Ord π¦) β (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯)) |
7 | 4, 5, 6 | syl2an 597 |
. . . 4
β’ ((π₯ β On β§ π¦ β On) β (π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯)) |
8 | | sdomirr 9114 |
. . . . . . . . 9
β’ Β¬
(π
1βπ¦) βΊ (π
1βπ¦) |
9 | | r1sdom 9769 |
. . . . . . . . . 10
β’ ((π¦ β On β§ π₯ β π¦) β (π
1βπ₯) βΊ
(π
1βπ¦)) |
10 | | breq1 5152 |
. . . . . . . . . 10
β’
((π
1βπ₯) = (π
1βπ¦) β
((π
1βπ₯) βΊ (π
1βπ¦) β
(π
1βπ¦) βΊ (π
1βπ¦))) |
11 | 9, 10 | syl5ibcom 244 |
. . . . . . . . 9
β’ ((π¦ β On β§ π₯ β π¦) β ((π
1βπ₯) =
(π
1βπ¦) β (π
1βπ¦) βΊ
(π
1βπ¦))) |
12 | 8, 11 | mtoi 198 |
. . . . . . . 8
β’ ((π¦ β On β§ π₯ β π¦) β Β¬
(π
1βπ₯) = (π
1βπ¦)) |
13 | 12 | 3adant1 1131 |
. . . . . . 7
β’ ((π₯ β On β§ π¦ β On β§ π₯ β π¦) β Β¬
(π
1βπ₯) = (π
1βπ¦)) |
14 | 13 | pm2.21d 121 |
. . . . . 6
β’ ((π₯ β On β§ π¦ β On β§ π₯ β π¦) β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦)) |
15 | 14 | 3expia 1122 |
. . . . 5
β’ ((π₯ β On β§ π¦ β On) β (π₯ β π¦ β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦))) |
16 | | ax-1 6 |
. . . . . 6
β’ (π₯ = π¦ β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦)) |
17 | 16 | a1i 11 |
. . . . 5
β’ ((π₯ β On β§ π¦ β On) β (π₯ = π¦ β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦))) |
18 | | r1sdom 9769 |
. . . . . . . . . 10
β’ ((π₯ β On β§ π¦ β π₯) β (π
1βπ¦) βΊ
(π
1βπ₯)) |
19 | | breq2 5153 |
. . . . . . . . . 10
β’
((π
1βπ₯) = (π
1βπ¦) β
((π
1βπ¦) βΊ (π
1βπ₯) β
(π
1βπ¦) βΊ (π
1βπ¦))) |
20 | 18, 19 | syl5ibcom 244 |
. . . . . . . . 9
β’ ((π₯ β On β§ π¦ β π₯) β ((π
1βπ₯) =
(π
1βπ¦) β (π
1βπ¦) βΊ
(π
1βπ¦))) |
21 | 8, 20 | mtoi 198 |
. . . . . . . 8
β’ ((π₯ β On β§ π¦ β π₯) β Β¬
(π
1βπ₯) = (π
1βπ¦)) |
22 | 21 | 3adant2 1132 |
. . . . . . 7
β’ ((π₯ β On β§ π¦ β On β§ π¦ β π₯) β Β¬
(π
1βπ₯) = (π
1βπ¦)) |
23 | 22 | pm2.21d 121 |
. . . . . 6
β’ ((π₯ β On β§ π¦ β On β§ π¦ β π₯) β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦)) |
24 | 23 | 3expia 1122 |
. . . . 5
β’ ((π₯ β On β§ π¦ β On) β (π¦ β π₯ β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦))) |
25 | 15, 17, 24 | 3jaod 1429 |
. . . 4
β’ ((π₯ β On β§ π¦ β On) β ((π₯ β π¦ β¨ π₯ = π¦ β¨ π¦ β π₯) β ((π
1βπ₯) =
(π
1βπ¦) β π₯ = π¦))) |
26 | 7, 25 | mpd 15 |
. . 3
β’ ((π₯ β On β§ π¦ β On) β
((π
1βπ₯) = (π
1βπ¦) β π₯ = π¦)) |
27 | 26 | rgen2 3198 |
. 2
β’
βπ₯ β On
βπ¦ β On
((π
1βπ₯) = (π
1βπ¦) β π₯ = π¦) |
28 | | dff13 7254 |
. 2
β’
(π
1:Onβ1-1βV β (π
1:OnβΆV
β§ βπ₯ β On
βπ¦ β On
((π
1βπ₯) = (π
1βπ¦) β π₯ = π¦))) |
29 | 3, 27, 28 | mpbir2an 710 |
1
β’
π
1:Onβ1-1βV |