Step | Hyp | Ref
| Expression |
1 | | f1omptsn.f |
. . . . 5
β’ πΉ = (π₯ β π΄ β¦ {π₯}) |
2 | | eqid 2732 |
. . . . . . 7
β’ {π₯} = {π₯} |
3 | | vsnex 5429 |
. . . . . . . 8
β’ {π₯} β V |
4 | | eqsbc1 3826 |
. . . . . . . 8
β’ ({π₯} β V β
([{π₯} / π’]π’ = {π₯} β {π₯} = {π₯})) |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
β’
([{π₯} / π’]π’ = {π₯} β {π₯} = {π₯}) |
6 | 2, 5 | mpbir 230 |
. . . . . 6
β’
[{π₯} / π’]π’ = {π₯} |
7 | | sbcel2 4415 |
. . . . . . . 8
β’
([{π₯} / π’]π₯ β π΄ β π₯ β β¦{π₯} / π’β¦π΄) |
8 | | csbconstg 3912 |
. . . . . . . . . 10
β’ ({π₯} β V β
β¦{π₯} / π’β¦π΄ = π΄) |
9 | 3, 8 | ax-mp 5 |
. . . . . . . . 9
β’
β¦{π₯} /
π’β¦π΄ = π΄ |
10 | 9 | eleq2i 2825 |
. . . . . . . 8
β’ (π₯ β β¦{π₯} / π’β¦π΄ β π₯ β π΄) |
11 | 7, 10 | bitri 274 |
. . . . . . 7
β’
([{π₯} / π’]π₯ β π΄ β π₯ β π΄) |
12 | | f1omptsn.r |
. . . . . . . . . . . . . 14
β’ π
= {π’ β£ βπ₯ β π΄ π’ = {π₯}} |
13 | 12 | eqabri 2877 |
. . . . . . . . . . . . 13
β’ (π’ β π
β βπ₯ β π΄ π’ = {π₯}) |
14 | | df-rex 3071 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ π’ = {π₯} β βπ₯(π₯ β π΄ β§ π’ = {π₯})) |
15 | 13, 14 | sylbbr 235 |
. . . . . . . . . . . 12
β’
(βπ₯(π₯ β π΄ β§ π’ = {π₯}) β π’ β π
) |
16 | 15 | 19.23bi 2184 |
. . . . . . . . . . 11
β’ ((π₯ β π΄ β§ π’ = {π₯}) β π’ β π
) |
17 | 16 | sbcth 3792 |
. . . . . . . . . 10
β’ ({π₯} β V β [{π₯} / π’]((π₯ β π΄ β§ π’ = {π₯}) β π’ β π
)) |
18 | 3, 17 | ax-mp 5 |
. . . . . . . . 9
β’
[{π₯} / π’]((π₯ β π΄ β§ π’ = {π₯}) β π’ β π
) |
19 | | sbcimg 3828 |
. . . . . . . . . 10
β’ ({π₯} β V β
([{π₯} / π’]((π₯ β π΄ β§ π’ = {π₯}) β π’ β π
) β ([{π₯} / π’](π₯ β π΄ β§ π’ = {π₯}) β [{π₯} / π’]π’ β π
))) |
20 | 3, 19 | ax-mp 5 |
. . . . . . . . 9
β’
([{π₯} / π’]((π₯ β π΄ β§ π’ = {π₯}) β π’ β π
) β ([{π₯} / π’](π₯ β π΄ β§ π’ = {π₯}) β [{π₯} / π’]π’ β π
)) |
21 | 18, 20 | mpbi 229 |
. . . . . . . 8
β’
([{π₯} / π’](π₯ β π΄ β§ π’ = {π₯}) β [{π₯} / π’]π’ β π
) |
22 | | sbcan 3829 |
. . . . . . . 8
β’
([{π₯} / π’](π₯ β π΄ β§ π’ = {π₯}) β ([{π₯} / π’]π₯ β π΄ β§ [{π₯} / π’]π’ = {π₯})) |
23 | | sbcel1v 3848 |
. . . . . . . 8
β’
([{π₯} / π’]π’ β π
β {π₯} β π
) |
24 | 21, 22, 23 | 3imtr3i 290 |
. . . . . . 7
β’
(([{π₯} /
π’]π₯ β π΄ β§ [{π₯} / π’]π’ = {π₯}) β {π₯} β π
) |
25 | 11, 24 | sylanbr 582 |
. . . . . 6
β’ ((π₯ β π΄ β§ [{π₯} / π’]π’ = {π₯}) β {π₯} β π
) |
26 | 6, 25 | mpan2 689 |
. . . . 5
β’ (π₯ β π΄ β {π₯} β π
) |
27 | 1, 26 | fmpti 7113 |
. . . 4
β’ πΉ:π΄βΆπ
|
28 | 1 | fvmpt2 7009 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ {π₯} β π
) β (πΉβπ₯) = {π₯}) |
29 | 26, 28 | mpdan 685 |
. . . . . . . 8
β’ (π₯ β π΄ β (πΉβπ₯) = {π₯}) |
30 | | sneq 4638 |
. . . . . . . . 9
β’ (π₯ = π¦ β {π₯} = {π¦}) |
31 | 30, 1, 3 | fvmpt3i 7003 |
. . . . . . . 8
β’ (π¦ β π΄ β (πΉβπ¦) = {π¦}) |
32 | 29, 31 | eqeqan12d 2746 |
. . . . . . 7
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΉβπ₯) = (πΉβπ¦) β {π₯} = {π¦})) |
33 | | vex 3478 |
. . . . . . . 8
β’ π₯ β V |
34 | | sneqbg 4844 |
. . . . . . . 8
β’ (π₯ β V β ({π₯} = {π¦} β π₯ = π¦)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . 7
β’ ({π₯} = {π¦} β π₯ = π¦) |
36 | 32, 35 | bitrdi 286 |
. . . . . 6
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦)) |
37 | 36 | biimpd 228 |
. . . . 5
β’ ((π₯ β π΄ β§ π¦ β π΄) β ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦)) |
38 | 37 | rgen2 3197 |
. . . 4
β’
βπ₯ β
π΄ βπ¦ β π΄ ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦) |
39 | | dff13 7256 |
. . . 4
β’ (πΉ:π΄β1-1βπ
β (πΉ:π΄βΆπ
β§ βπ₯ β π΄ βπ¦ β π΄ ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦))) |
40 | 27, 38, 39 | mpbir2an 709 |
. . 3
β’ πΉ:π΄β1-1βπ
|
41 | | f1f1orn 6844 |
. . 3
β’ (πΉ:π΄β1-1βπ
β πΉ:π΄β1-1-ontoβran
πΉ) |
42 | 40, 41 | ax-mp 5 |
. 2
β’ πΉ:π΄β1-1-ontoβran
πΉ |
43 | | rnmptsn 36308 |
. . . 4
β’ ran
(π₯ β π΄ β¦ {π₯}) = {π’ β£ βπ₯ β π΄ π’ = {π₯}} |
44 | 1 | rneqi 5936 |
. . . 4
β’ ran πΉ = ran (π₯ β π΄ β¦ {π₯}) |
45 | 43, 44, 12 | 3eqtr4i 2770 |
. . 3
β’ ran πΉ = π
|
46 | | f1oeq3 6823 |
. . 3
β’ (ran
πΉ = π
β (πΉ:π΄β1-1-ontoβran
πΉ β πΉ:π΄β1-1-ontoβπ
)) |
47 | 45, 46 | ax-mp 5 |
. 2
β’ (πΉ:π΄β1-1-ontoβran
πΉ β πΉ:π΄β1-1-ontoβπ
) |
48 | 42, 47 | mpbi 229 |
1
β’ πΉ:π΄β1-1-ontoβπ
|