Step | Hyp | Ref
| Expression |
1 | | fpwrelmap.3 |
. . 3
β’ π = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
2 | | fpwrelmap.1 |
. . . . . 6
β’ π΄ β V |
3 | 2 | a1i 11 |
. . . . 5
β’ (π β (π« π΅ βm π΄) β π΄ β V) |
4 | | simpr 486 |
. . . . . . . . 9
β’ (((π β (π« π΅ βm π΄) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β π¦ β (πβπ₯)) |
5 | | elmapi 8794 |
. . . . . . . . . . 11
β’ (π β (π« π΅ βm π΄) β π:π΄βΆπ« π΅) |
6 | 5 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β (π« π΅ βm π΄) β§ π₯ β π΄) β (πβπ₯) β π« π΅) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ (((π β (π« π΅ βm π΄) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β (πβπ₯) β π« π΅) |
8 | | elelpwi 4575 |
. . . . . . . . 9
β’ ((π¦ β (πβπ₯) β§ (πβπ₯) β π« π΅) β π¦ β π΅) |
9 | 4, 7, 8 | syl2anc 585 |
. . . . . . . 8
β’ (((π β (π« π΅ βm π΄) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β π¦ β π΅) |
10 | 9 | ex 414 |
. . . . . . 7
β’ ((π β (π« π΅ βm π΄) β§ π₯ β π΄) β (π¦ β (πβπ₯) β π¦ β π΅)) |
11 | 10 | alrimiv 1931 |
. . . . . 6
β’ ((π β (π« π΅ βm π΄) β§ π₯ β π΄) β βπ¦(π¦ β (πβπ₯) β π¦ β π΅)) |
12 | | abss 4022 |
. . . . . . 7
β’ ({π¦ β£ π¦ β (πβπ₯)} β π΅ β βπ¦(π¦ β (πβπ₯) β π¦ β π΅)) |
13 | | fpwrelmap.2 |
. . . . . . . 8
β’ π΅ β V |
14 | 13 | ssex 5283 |
. . . . . . 7
β’ ({π¦ β£ π¦ β (πβπ₯)} β π΅ β {π¦ β£ π¦ β (πβπ₯)} β V) |
15 | 12, 14 | sylbir 234 |
. . . . . 6
β’
(βπ¦(π¦ β (πβπ₯) β π¦ β π΅) β {π¦ β£ π¦ β (πβπ₯)} β V) |
16 | 11, 15 | syl 17 |
. . . . 5
β’ ((π β (π« π΅ βm π΄) β§ π₯ β π΄) β {π¦ β£ π¦ β (πβπ₯)} β V) |
17 | 3, 16 | opabex3d 7903 |
. . . 4
β’ (π β (π« π΅ βm π΄) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β V) |
18 | 17 | adantl 483 |
. . 3
β’
((β€ β§ π
β (π« π΅
βm π΄))
β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β V) |
19 | 2 | mptex 7178 |
. . . 4
β’ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) β V |
20 | 19 | a1i 11 |
. . 3
β’
((β€ β§ π
β π« (π΄ Γ
π΅)) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) β V) |
21 | 10 | imdistanda 573 |
. . . . . . . . . 10
β’ (π β (π« π΅ βm π΄) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β (π₯ β π΄ β§ π¦ β π΅))) |
22 | 21 | ssopab2dv 5513 |
. . . . . . . . 9
β’ (π β (π« π΅ βm π΄) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β π΅)}) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β π΅)}) |
24 | | simpr 486 |
. . . . . . . 8
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
25 | | df-xp 5644 |
. . . . . . . . 9
β’ (π΄ Γ π΅) = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β π΅)} |
26 | 25 | a1i 11 |
. . . . . . . 8
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π΄ Γ π΅) = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β π΅)}) |
27 | 23, 24, 26 | 3sstr4d 3996 |
. . . . . . 7
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π β (π΄ Γ π΅)) |
28 | | velpw 4570 |
. . . . . . 7
β’ (π β π« (π΄ Γ π΅) β π β (π΄ Γ π΅)) |
29 | 27, 28 | sylibr 233 |
. . . . . 6
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π β π« (π΄ Γ π΅)) |
30 | 5 | feqmptd 6915 |
. . . . . . . 8
β’ (π β (π« π΅ βm π΄) β π = (π₯ β π΄ β¦ (πβπ₯))) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π = (π₯ β π΄ β¦ (πβπ₯))) |
32 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯ π β (π« π΅ βm π΄) |
33 | | nfopab1 5180 |
. . . . . . . . . 10
β’
β²π₯{β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
34 | 33 | nfeq2 2925 |
. . . . . . . . 9
β’
β²π₯ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
35 | 32, 34 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
36 | | df-rab 3411 |
. . . . . . . . . 10
β’ {π¦ β π΅ β£ π₯ππ¦} = {π¦ β£ (π¦ β π΅ β§ π₯ππ¦)} |
37 | 36 | a1i 11 |
. . . . . . . . 9
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β {π¦ β π΅ β£ π₯ππ¦} = {π¦ β£ (π¦ β π΅ β§ π₯ππ¦)}) |
38 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π¦ π β (π« π΅ βm π΄) |
39 | | nfopab2 5181 |
. . . . . . . . . . . . 13
β’
β²π¦{β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
40 | 39 | nfeq2 2925 |
. . . . . . . . . . . 12
β’
β²π¦ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
41 | 38, 40 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π¦(π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
42 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π¦ π₯ β π΄ |
43 | 41, 42 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) |
44 | 9 | adantllr 718 |
. . . . . . . . . . . . 13
β’ ((((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β π¦ β π΅) |
45 | | df-br 5111 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ππ¦ β β¨π₯, π¦β© β π) |
46 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (β¨π₯, π¦β© β π β β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) |
47 | | opabidw 5486 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (π₯ β π΄ β§ π¦ β (πβπ₯))) |
48 | 46, 47 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
β’ (π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (β¨π₯, π¦β© β π β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
49 | 45, 48 | bitrid 283 |
. . . . . . . . . . . . . . . 16
β’ (π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (π₯ππ¦ β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
50 | 49 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π₯ππ¦ β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
51 | | elfvdm 6884 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (πβπ₯) β π₯ β dom π) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (π« π΅ βm π΄) β§ π¦ β (πβπ₯)) β π₯ β dom π) |
53 | 5 | fdmd 6684 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π« π΅ βm π΄) β dom π = π΄) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (π« π΅ βm π΄) β§ π¦ β (πβπ₯)) β dom π = π΄) |
55 | 52, 54 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (π« π΅ βm π΄) β§ π¦ β (πβπ₯)) β π₯ β π΄) |
56 | 55 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π« π΅ βm π΄) β (π¦ β (πβπ₯) β π₯ β π΄)) |
57 | 56 | pm4.71rd 564 |
. . . . . . . . . . . . . . . 16
β’ (π β (π« π΅ βm π΄) β (π¦ β (πβπ₯) β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
58 | 57 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π¦ β (πβπ₯) β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
59 | 50, 58 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π₯ππ¦ β π¦ β (πβπ₯))) |
60 | 59 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β π₯ππ¦) |
61 | 44, 60 | jca 513 |
. . . . . . . . . . . 12
β’ ((((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β (π¦ β π΅ β§ π₯ππ¦)) |
62 | 61 | ex 414 |
. . . . . . . . . . 11
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π¦ β (πβπ₯) β (π¦ β π΅ β§ π₯ππ¦))) |
63 | 59 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π₯ππ¦ β π¦ β (πβπ₯))) |
64 | 63 | adantld 492 |
. . . . . . . . . . 11
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β ((π¦ β π΅ β§ π₯ππ¦) β π¦ β (πβπ₯))) |
65 | 62, 64 | impbid 211 |
. . . . . . . . . 10
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (π¦ β (πβπ₯) β (π¦ β π΅ β§ π₯ππ¦))) |
66 | 43, 65 | abbid 2808 |
. . . . . . . . 9
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β {π¦ β£ π¦ β (πβπ₯)} = {π¦ β£ (π¦ β π΅ β§ π₯ππ¦)}) |
67 | | abid2 2876 |
. . . . . . . . . 10
β’ {π¦ β£ π¦ β (πβπ₯)} = (πβπ₯) |
68 | 67 | a1i 11 |
. . . . . . . . 9
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β {π¦ β£ π¦ β (πβπ₯)} = (πβπ₯)) |
69 | 37, 66, 68 | 3eqtr2rd 2784 |
. . . . . . . 8
β’ (((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π₯ β π΄) β (πβπ₯) = {π¦ β π΅ β£ π₯ππ¦}) |
70 | 35, 69 | mpteq2da 5208 |
. . . . . . 7
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π₯ β π΄ β¦ (πβπ₯)) = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
71 | 31, 70 | eqtrd 2777 |
. . . . . 6
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
72 | 29, 71 | jca 513 |
. . . . 5
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
73 | | ssrab2 4042 |
. . . . . . . . . . . 12
β’ {π¦ β π΅ β£ π₯ππ¦} β π΅ |
74 | 13, 73 | elpwi2 5308 |
. . . . . . . . . . 11
β’ {π¦ β π΅ β£ π₯ππ¦} β π« π΅ |
75 | 74 | a1i 11 |
. . . . . . . . . 10
β’ ((π β π« (π΄ Γ π΅) β§ π₯ β π΄) β {π¦ β π΅ β£ π₯ππ¦} β π« π΅) |
76 | 75 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β π« (π΄ Γ π΅) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}):π΄βΆπ« π΅) |
77 | 76 | adantr 482 |
. . . . . . . 8
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}):π΄βΆπ« π΅) |
78 | | simpr 486 |
. . . . . . . . 9
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
79 | 78 | feq1d 6658 |
. . . . . . . 8
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π:π΄βΆπ« π΅ β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}):π΄βΆπ« π΅)) |
80 | 77, 79 | mpbird 257 |
. . . . . . 7
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π:π΄βΆπ« π΅) |
81 | 13 | pwex 5340 |
. . . . . . . 8
β’ π«
π΅ β V |
82 | 81, 2 | elmap 8816 |
. . . . . . 7
β’ (π β (π« π΅ βm π΄) β π:π΄βΆπ« π΅) |
83 | 80, 82 | sylibr 233 |
. . . . . 6
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (π« π΅ βm π΄)) |
84 | | elpwi 4572 |
. . . . . . . . . 10
β’ (π β π« (π΄ Γ π΅) β π β (π΄ Γ π΅)) |
85 | 84 | adantr 482 |
. . . . . . . . 9
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (π΄ Γ π΅)) |
86 | | xpss 5654 |
. . . . . . . . 9
β’ (π΄ Γ π΅) β (V Γ V) |
87 | 85, 86 | sstrdi 3961 |
. . . . . . . 8
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (V Γ V)) |
88 | | df-rel 5645 |
. . . . . . . 8
β’ (Rel
π β π β (V Γ V)) |
89 | 87, 88 | sylibr 233 |
. . . . . . 7
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β Rel π) |
90 | | relopabv 5782 |
. . . . . . . 8
β’ Rel
{β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
91 | 90 | a1i 11 |
. . . . . . 7
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β Rel {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
92 | | id 22 |
. . . . . . 7
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
93 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯ π β π« (π΄ Γ π΅) |
94 | | nfmpt1 5218 |
. . . . . . . . . 10
β’
β²π₯(π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) |
95 | 94 | nfeq2 2925 |
. . . . . . . . 9
β’
β²π₯ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) |
96 | 93, 95 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
97 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦ π β π« (π΄ Γ π΅) |
98 | 42 | nfci 2891 |
. . . . . . . . . . 11
β’
β²π¦π΄ |
99 | | nfrab1 3429 |
. . . . . . . . . . 11
β’
β²π¦{π¦ β π΅ β£ π₯ππ¦} |
100 | 98, 99 | nfmpt 5217 |
. . . . . . . . . 10
β’
β²π¦(π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) |
101 | 100 | nfeq2 2925 |
. . . . . . . . 9
β’
β²π¦ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) |
102 | 97, 101 | nfan 1903 |
. . . . . . . 8
β’
β²π¦(π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
103 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯π |
104 | | nfcv 2908 |
. . . . . . . 8
β’
β²π¦π |
105 | | brelg 31570 |
. . . . . . . . . . . . . . . 16
β’ ((π β (π΄ Γ π΅) β§ π₯ππ¦) β (π₯ β π΄ β§ π¦ β π΅)) |
106 | 84, 105 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π β π« (π΄ Γ π΅) β§ π₯ππ¦) β (π₯ β π΄ β§ π¦ β π΅)) |
107 | 106 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β (π₯ β π΄ β§ π¦ β π΅)) |
108 | 107 | simpld 496 |
. . . . . . . . . . . . 13
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β π₯ β π΄) |
109 | 107 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β π¦ β π΅) |
110 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β π₯ππ¦) |
111 | 78 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (πβπ₯) = ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})βπ₯)) |
112 | 13 | rabex 5294 |
. . . . . . . . . . . . . . . . . . 19
β’ {π¦ β π΅ β£ π₯ππ¦} β V |
113 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) |
114 | 113 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β π΄ β§ {π¦ β π΅ β£ π₯ππ¦} β V) β ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})βπ₯) = {π¦ β π΅ β£ π₯ππ¦}) |
115 | 112, 114 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π΄ β ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})βπ₯) = {π¦ β π΅ β£ π₯ππ¦}) |
116 | 111, 115 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ β π΄) β (πβπ₯) = {π¦ β π΅ β£ π₯ππ¦}) |
117 | 116 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ β π΄) β (π¦ β (πβπ₯) β π¦ β {π¦ β π΅ β£ π₯ππ¦})) |
118 | | rabid 3430 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β {π¦ β π΅ β£ π₯ππ¦} β (π¦ β π΅ β§ π₯ππ¦)) |
119 | 117, 118 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ β π΄) β (π¦ β (πβπ₯) β (π¦ β π΅ β§ π₯ππ¦))) |
120 | 108, 119 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β (π¦ β (πβπ₯) β (π¦ β π΅ β§ π₯ππ¦))) |
121 | 109, 110,
120 | mpbir2and 712 |
. . . . . . . . . . . . 13
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β π¦ β (πβπ₯)) |
122 | 108, 121 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ππ¦) β (π₯ β π΄ β§ π¦ β (πβπ₯))) |
123 | 122 | ex 414 |
. . . . . . . . . . 11
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π₯ππ¦ β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
124 | 119 | simplbda 501 |
. . . . . . . . . . . 12
β’ ((((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π₯ β π΄) β§ π¦ β (πβπ₯)) β π₯ππ¦) |
125 | 124 | expl 459 |
. . . . . . . . . . 11
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β π₯ππ¦)) |
126 | 123, 125 | impbid 211 |
. . . . . . . . . 10
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π₯ππ¦ β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
127 | 45, 126 | bitr3id 285 |
. . . . . . . . 9
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (β¨π₯, π¦β© β π β (π₯ β π΄ β§ π¦ β (πβπ₯)))) |
128 | 127, 47 | bitr4di 289 |
. . . . . . . 8
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (β¨π₯, π¦β© β π β β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) |
129 | 96, 102, 103, 104, 33, 39, 128 | eqrelrd2 31577 |
. . . . . . 7
β’ (((Rel
π β§ Rel {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ (π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
130 | 89, 91, 92, 129 | syl21anc 837 |
. . . . . 6
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
131 | 83, 130 | jca 513 |
. . . . 5
β’ ((π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) |
132 | 72, 131 | impbii 208 |
. . . 4
β’ ((π β (π« π΅ βm π΄) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
133 | 132 | a1i 11 |
. . 3
β’ (β€
β ((π β
(π« π΅
βm π΄) β§
π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π β π« (π΄ Γ π΅) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})))) |
134 | 1, 18, 20, 133 | f1od 7610 |
. 2
β’ (β€
β π:(π« π΅ βm π΄)β1-1-ontoβπ« (π΄ Γ π΅)) |
135 | 134 | mptru 1549 |
1
β’ π:(π« π΅ βm π΄)β1-1-ontoβπ« (π΄ Γ π΅) |