Step | Hyp | Ref
| Expression |
1 | | mapsnd.1 |
. . . 4
β’ (π β π΄ β π) |
2 | | snex 5389 |
. . . . 5
β’ {π΅} β V |
3 | 2 | a1i 11 |
. . . 4
β’ (π β {π΅} β V) |
4 | 1, 3 | elmapd 8782 |
. . 3
β’ (π β (π β (π΄ βm {π΅}) β π:{π΅}βΆπ΄)) |
5 | | ffn 6669 |
. . . . . . . . 9
β’ (π:{π΅}βΆπ΄ β π Fn {π΅}) |
6 | | mapsnd.2 |
. . . . . . . . . 10
β’ (π β π΅ β π) |
7 | | snidg 4621 |
. . . . . . . . . 10
β’ (π΅ β π β π΅ β {π΅}) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β {π΅}) |
9 | | fneu 6613 |
. . . . . . . . 9
β’ ((π Fn {π΅} β§ π΅ β {π΅}) β β!π¦ π΅ππ¦) |
10 | 5, 8, 9 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ π:{π΅}βΆπ΄) β β!π¦ π΅ππ¦) |
11 | | euabsn 4688 |
. . . . . . . . . 10
β’
(β!π¦ π΅ππ¦ β βπ¦{π¦ β£ π΅ππ¦} = {π¦}) |
12 | | frel 6674 |
. . . . . . . . . . . . . 14
β’ (π:{π΅}βΆπ΄ β Rel π) |
13 | | relimasn 6037 |
. . . . . . . . . . . . . 14
β’ (Rel
π β (π β {π΅}) = {π¦ β£ π΅ππ¦}) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
β’ (π:{π΅}βΆπ΄ β (π β {π΅}) = {π¦ β£ π΅ππ¦}) |
15 | | fdm 6678 |
. . . . . . . . . . . . . . 15
β’ (π:{π΅}βΆπ΄ β dom π = {π΅}) |
16 | 15 | imaeq2d 6014 |
. . . . . . . . . . . . . 14
β’ (π:{π΅}βΆπ΄ β (π β dom π) = (π β {π΅})) |
17 | | imadmrn 6024 |
. . . . . . . . . . . . . 14
β’ (π β dom π) = ran π |
18 | 16, 17 | eqtr3di 2788 |
. . . . . . . . . . . . 13
β’ (π:{π΅}βΆπ΄ β (π β {π΅}) = ran π) |
19 | 14, 18 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (π:{π΅}βΆπ΄ β {π¦ β£ π΅ππ¦} = ran π) |
20 | 19 | eqeq1d 2735 |
. . . . . . . . . . 11
β’ (π:{π΅}βΆπ΄ β ({π¦ β£ π΅ππ¦} = {π¦} β ran π = {π¦})) |
21 | 20 | exbidv 1925 |
. . . . . . . . . 10
β’ (π:{π΅}βΆπ΄ β (βπ¦{π¦ β£ π΅ππ¦} = {π¦} β βπ¦ran π = {π¦})) |
22 | 11, 21 | bitrid 283 |
. . . . . . . . 9
β’ (π:{π΅}βΆπ΄ β (β!π¦ π΅ππ¦ β βπ¦ran π = {π¦})) |
23 | 22 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π:{π΅}βΆπ΄) β (β!π¦ π΅ππ¦ β βπ¦ran π = {π¦})) |
24 | 10, 23 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π:{π΅}βΆπ΄) β βπ¦ran π = {π¦}) |
25 | | frn 6676 |
. . . . . . . . . . . . 13
β’ (π:{π΅}βΆπ΄ β ran π β π΄) |
26 | 25 | sseld 3944 |
. . . . . . . . . . . 12
β’ (π:{π΅}βΆπ΄ β (π¦ β ran π β π¦ β π΄)) |
27 | | vsnid 4624 |
. . . . . . . . . . . . 13
β’ π¦ β {π¦} |
28 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (ran
π = {π¦} β (π¦ β ran π β π¦ β {π¦})) |
29 | 27, 28 | mpbiri 258 |
. . . . . . . . . . . 12
β’ (ran
π = {π¦} β π¦ β ran π) |
30 | 26, 29 | impel 507 |
. . . . . . . . . . 11
β’ ((π:{π΅}βΆπ΄ β§ ran π = {π¦}) β π¦ β π΄) |
31 | 30 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β π¦ β π΄) |
32 | | ffrn 6683 |
. . . . . . . . . . . . . 14
β’ (π:{π΅}βΆπ΄ β π:{π΅}βΆran π) |
33 | | feq3 6652 |
. . . . . . . . . . . . . 14
β’ (ran
π = {π¦} β (π:{π΅}βΆran π β π:{π΅}βΆ{π¦})) |
34 | 32, 33 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (π:{π΅}βΆπ΄ β (ran π = {π¦} β π:{π΅}βΆ{π¦})) |
35 | 34 | imp 408 |
. . . . . . . . . . . 12
β’ ((π:{π΅}βΆπ΄ β§ ran π = {π¦}) β π:{π΅}βΆ{π¦}) |
36 | 35 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β π:{π΅}βΆ{π¦}) |
37 | 6 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β π΅ β π) |
38 | | vex 3448 |
. . . . . . . . . . . 12
β’ π¦ β V |
39 | | fsng 7084 |
. . . . . . . . . . . 12
β’ ((π΅ β π β§ π¦ β V) β (π:{π΅}βΆ{π¦} β π = {β¨π΅, π¦β©})) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β (π:{π΅}βΆ{π¦} β π = {β¨π΅, π¦β©})) |
41 | 36, 40 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β π = {β¨π΅, π¦β©}) |
42 | 31, 41 | jca 513 |
. . . . . . . . 9
β’ (((π β§ π:{π΅}βΆπ΄) β§ ran π = {π¦}) β (π¦ β π΄ β§ π = {β¨π΅, π¦β©})) |
43 | 42 | ex 414 |
. . . . . . . 8
β’ ((π β§ π:{π΅}βΆπ΄) β (ran π = {π¦} β (π¦ β π΄ β§ π = {β¨π΅, π¦β©}))) |
44 | 43 | eximdv 1921 |
. . . . . . 7
β’ ((π β§ π:{π΅}βΆπ΄) β (βπ¦ran π = {π¦} β βπ¦(π¦ β π΄ β§ π = {β¨π΅, π¦β©}))) |
45 | 24, 44 | mpd 15 |
. . . . . 6
β’ ((π β§ π:{π΅}βΆπ΄) β βπ¦(π¦ β π΄ β§ π = {β¨π΅, π¦β©})) |
46 | | df-rex 3071 |
. . . . . 6
β’
(βπ¦ β
π΄ π = {β¨π΅, π¦β©} β βπ¦(π¦ β π΄ β§ π = {β¨π΅, π¦β©})) |
47 | 45, 46 | sylibr 233 |
. . . . 5
β’ ((π β§ π:{π΅}βΆπ΄) β βπ¦ β π΄ π = {β¨π΅, π¦β©}) |
48 | 47 | ex 414 |
. . . 4
β’ (π β (π:{π΅}βΆπ΄ β βπ¦ β π΄ π = {β¨π΅, π¦β©})) |
49 | | f1osng 6826 |
. . . . . . . . . . 11
β’ ((π΅ β π β§ π¦ β V) β {β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦}) |
50 | 6, 38, 49 | sylancl 587 |
. . . . . . . . . 10
β’ (π β {β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦}) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π = {β¨π΅, π¦β©}) β {β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦}) |
52 | | f1oeq1 6773 |
. . . . . . . . . . 11
β’ (π = {β¨π΅, π¦β©} β (π:{π΅}β1-1-ontoβ{π¦} β {β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦})) |
53 | 52 | bicomd 222 |
. . . . . . . . . 10
β’ (π = {β¨π΅, π¦β©} β ({β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦} β π:{π΅}β1-1-ontoβ{π¦})) |
54 | 53 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π = {β¨π΅, π¦β©}) β ({β¨π΅, π¦β©}:{π΅}β1-1-ontoβ{π¦} β π:{π΅}β1-1-ontoβ{π¦})) |
55 | 51, 54 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π = {β¨π΅, π¦β©}) β π:{π΅}β1-1-ontoβ{π¦}) |
56 | | f1of 6785 |
. . . . . . . 8
β’ (π:{π΅}β1-1-ontoβ{π¦} β π:{π΅}βΆ{π¦}) |
57 | 55, 56 | syl 17 |
. . . . . . 7
β’ ((π β§ π = {β¨π΅, π¦β©}) β π:{π΅}βΆ{π¦}) |
58 | 57 | 3adant2 1132 |
. . . . . 6
β’ ((π β§ π¦ β π΄ β§ π = {β¨π΅, π¦β©}) β π:{π΅}βΆ{π¦}) |
59 | | snssi 4769 |
. . . . . . 7
β’ (π¦ β π΄ β {π¦} β π΄) |
60 | 59 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β§ π¦ β π΄ β§ π = {β¨π΅, π¦β©}) β {π¦} β π΄) |
61 | 58, 60 | fssd 6687 |
. . . . 5
β’ ((π β§ π¦ β π΄ β§ π = {β¨π΅, π¦β©}) β π:{π΅}βΆπ΄) |
62 | 61 | rexlimdv3a 3153 |
. . . 4
β’ (π β (βπ¦ β π΄ π = {β¨π΅, π¦β©} β π:{π΅}βΆπ΄)) |
63 | 48, 62 | impbid 211 |
. . 3
β’ (π β (π:{π΅}βΆπ΄ β βπ¦ β π΄ π = {β¨π΅, π¦β©})) |
64 | 4, 63 | bitrd 279 |
. 2
β’ (π β (π β (π΄ βm {π΅}) β βπ¦ β π΄ π = {β¨π΅, π¦β©})) |
65 | 64 | abbi2dv 2868 |
1
β’ (π β (π΄ βm {π΅}) = {π β£ βπ¦ β π΄ π = {β¨π΅, π¦β©}}) |