Step | Hyp | Ref
| Expression |
1 | | oacl 8485 |
. . . 4
β’ ((π΄ β On β§ π₯ β On) β (π΄ +o π₯) β On) |
2 | | oaword1 8503 |
. . . . 5
β’ ((π΄ β On β§ π₯ β On) β π΄ β (π΄ +o π₯)) |
3 | | ontri1 6355 |
. . . . . 6
β’ ((π΄ β On β§ (π΄ +o π₯) β On) β (π΄ β (π΄ +o π₯) β Β¬ (π΄ +o π₯) β π΄)) |
4 | 1, 3 | syldan 592 |
. . . . 5
β’ ((π΄ β On β§ π₯ β On) β (π΄ β (π΄ +o π₯) β Β¬ (π΄ +o π₯) β π΄)) |
5 | 2, 4 | mpbid 231 |
. . . 4
β’ ((π΄ β On β§ π₯ β On) β Β¬ (π΄ +o π₯) β π΄) |
6 | 1, 5 | eldifd 3925 |
. . 3
β’ ((π΄ β On β§ π₯ β On) β (π΄ +o π₯) β (On β π΄)) |
7 | 6 | ralrimiva 3140 |
. 2
β’ (π΄ β On β βπ₯ β On (π΄ +o π₯) β (On β π΄)) |
8 | | simpl 484 |
. . . . 5
β’ ((π΄ β On β§ π¦ β (On β π΄)) β π΄ β On) |
9 | | eldifi 4090 |
. . . . . 6
β’ (π¦ β (On β π΄) β π¦ β On) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π΄ β On β§ π¦ β (On β π΄)) β π¦ β On) |
11 | | eldifn 4091 |
. . . . . . 7
β’ (π¦ β (On β π΄) β Β¬ π¦ β π΄) |
12 | 11 | adantl 483 |
. . . . . 6
β’ ((π΄ β On β§ π¦ β (On β π΄)) β Β¬ π¦ β π΄) |
13 | | ontri1 6355 |
. . . . . . 7
β’ ((π΄ β On β§ π¦ β On) β (π΄ β π¦ β Β¬ π¦ β π΄)) |
14 | 10, 13 | syldan 592 |
. . . . . 6
β’ ((π΄ β On β§ π¦ β (On β π΄)) β (π΄ β π¦ β Β¬ π¦ β π΄)) |
15 | 12, 14 | mpbird 257 |
. . . . 5
β’ ((π΄ β On β§ π¦ β (On β π΄)) β π΄ β π¦) |
16 | | oawordeu 8506 |
. . . . 5
β’ (((π΄ β On β§ π¦ β On) β§ π΄ β π¦) β β!π₯ β On (π΄ +o π₯) = π¦) |
17 | 8, 10, 15, 16 | syl21anc 837 |
. . . 4
β’ ((π΄ β On β§ π¦ β (On β π΄)) β β!π₯ β On (π΄ +o π₯) = π¦) |
18 | | eqcom 2740 |
. . . . 5
β’ ((π΄ +o π₯) = π¦ β π¦ = (π΄ +o π₯)) |
19 | 18 | reubii 3361 |
. . . 4
β’
(β!π₯ β On
(π΄ +o π₯) = π¦ β β!π₯ β On π¦ = (π΄ +o π₯)) |
20 | 17, 19 | sylib 217 |
. . 3
β’ ((π΄ β On β§ π¦ β (On β π΄)) β β!π₯ β On π¦ = (π΄ +o π₯)) |
21 | 20 | ralrimiva 3140 |
. 2
β’ (π΄ β On β βπ¦ β (On β π΄)β!π₯ β On π¦ = (π΄ +o π₯)) |
22 | | eqid 2733 |
. . 3
β’ (π₯ β On β¦ (π΄ +o π₯)) = (π₯ β On β¦ (π΄ +o π₯)) |
23 | 22 | f1ompt 7063 |
. 2
β’ ((π₯ β On β¦ (π΄ +o π₯)):Onβ1-1-ontoβ(On
β π΄) β
(βπ₯ β On (π΄ +o π₯) β (On β π΄) β§ βπ¦ β (On β π΄)β!π₯ β On π¦ = (π΄ +o π₯))) |
24 | 7, 21, 23 | sylanbrc 584 |
1
β’ (π΄ β On β (π₯ β On β¦ (π΄ +o π₯)):Onβ1-1-ontoβ(On
β π΄)) |