Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’ (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
2 | | rfovd.b |
. . . . . . . 8
β’ (π β π΅ β π) |
3 | | ssrab2 4042 |
. . . . . . . . 9
β’ {π¦ β π΅ β£ π₯ππ¦} β π΅ |
4 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β {π¦ β π΅ β£ π₯ππ¦} β π΅) |
5 | 2, 4 | sselpwd 5288 |
. . . . . . 7
β’ (π β {π¦ β π΅ β£ π₯ππ¦} β π« π΅) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β {π¦ β π΅ β£ π₯ππ¦} β π« π΅) |
7 | 6 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}):π΄βΆπ« π΅) |
8 | 2 | pwexd 5339 |
. . . . . 6
β’ (π β π« π΅ β V) |
9 | | rfovd.a |
. . . . . 6
β’ (π β π΄ β π) |
10 | 8, 9 | elmapd 8786 |
. . . . 5
β’ (π β ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) β (π« π΅ βm π΄) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}):π΄βΆπ« π΅)) |
11 | 7, 10 | mpbird 257 |
. . . 4
β’ (π β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) β (π« π΅ βm π΄)) |
12 | 11 | adantr 482 |
. . 3
β’ ((π β§ π β π« (π΄ Γ π΅)) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) β (π« π΅ βm π΄)) |
13 | 9, 2 | xpexd 7690 |
. . . . 5
β’ (π β (π΄ Γ π΅) β V) |
14 | 13 | adantr 482 |
. . . 4
β’ ((π β§ π β (π« π΅ βm π΄)) β (π΄ Γ π΅) β V) |
15 | 8, 9 | elmapd 8786 |
. . . . . . . . . . . 12
β’ (π β (π β (π« π΅ βm π΄) β π:π΄βΆπ« π΅)) |
16 | 15 | biimpa 478 |
. . . . . . . . . . 11
β’ ((π β§ π β (π« π΅ βm π΄)) β π:π΄βΆπ« π΅) |
17 | 16 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ (((π β§ π β (π« π΅ βm π΄)) β§ π₯ β π΄) β (πβπ₯) β π« π΅) |
18 | 17 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π β (π« π΅ βm π΄)) β (π₯ β π΄ β (πβπ₯) β π« π΅)) |
19 | | elpwi 4572 |
. . . . . . . . . 10
β’ ((πβπ₯) β π« π΅ β (πβπ₯) β π΅) |
20 | 19 | sseld 3948 |
. . . . . . . . 9
β’ ((πβπ₯) β π« π΅ β (π¦ β (πβπ₯) β π¦ β π΅)) |
21 | 18, 20 | syl6 35 |
. . . . . . . 8
β’ ((π β§ π β (π« π΅ βm π΄)) β (π₯ β π΄ β (π¦ β (πβπ₯) β π¦ β π΅))) |
22 | 21 | imdistand 572 |
. . . . . . 7
β’ ((π β§ π β (π« π΅ βm π΄)) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β (π₯ β π΄ β§ π¦ β π΅))) |
23 | | trud 1552 |
. . . . . . 7
β’ ((π₯ β π΄ β§ π¦ β (πβπ₯)) β β€) |
24 | 22, 23 | jca2 515 |
. . . . . 6
β’ ((π β§ π β (π« π΅ βm π΄)) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β ((π₯ β π΄ β§ π¦ β π΅) β§ β€))) |
25 | 24 | ssopab2dv 5513 |
. . . . 5
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΅) β§ β€)}) |
26 | | opabssxp 5729 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΅) β§ β€)} β (π΄ Γ π΅) |
27 | 25, 26 | sstrdi 3961 |
. . . 4
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (π΄ Γ π΅)) |
28 | 14, 27 | sselpwd 5288 |
. . 3
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β π« (π΄ Γ π΅)) |
29 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π β (π« π΅ βm π΄)) |
30 | | elmapfn 8810 |
. . . . . 6
β’ (π β (π« π΅ βm π΄) β π Fn π΄) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π Fn π΄) |
32 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π΅ β π) |
33 | | rabexg 5293 |
. . . . . . 7
β’ (π΅ β π β {π¦ β π΅ β£ π₯ππ¦} β V) |
34 | 33 | ralrimivw 3148 |
. . . . . 6
β’ (π΅ β π β βπ₯ β π΄ {π¦ β π΅ β£ π₯ππ¦} β V) |
35 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯π΄ |
36 | 35 | fnmptf 6642 |
. . . . . 6
β’
(βπ₯ β
π΄ {π¦ β π΅ β£ π₯ππ¦} β V β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) Fn π΄) |
37 | 32, 34, 36 | 3syl 18 |
. . . . 5
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) Fn π΄) |
38 | | dfin5 3923 |
. . . . . . 7
β’ (π΅ β© (πβπ’)) = {π β π΅ β£ π β (πβπ’)} |
39 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) |
40 | | elmapi 8794 |
. . . . . . . . . . 11
β’ (π β (π« π΅ βm π΄) β π:π΄βΆπ« π΅) |
41 | 39, 40 | simpl2im 505 |
. . . . . . . . . 10
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β π:π΄βΆπ« π΅) |
42 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β π’ β π΄) |
43 | 41, 42 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (πβπ’) β π« π΅) |
44 | 43 | elpwid 4574 |
. . . . . . . 8
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (πβπ’) β π΅) |
45 | | sseqin2 4180 |
. . . . . . . 8
β’ ((πβπ’) β π΅ β (π΅ β© (πβπ’)) = (πβπ’)) |
46 | 44, 45 | sylib 217 |
. . . . . . 7
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (π΅ β© (πβπ’)) = (πβπ’)) |
47 | | ibar 530 |
. . . . . . . . 9
β’ (π’ β π΄ β (π β (πβπ’) β (π’ β π΄ β§ π β (πβπ’)))) |
48 | 47 | rabbidv 3418 |
. . . . . . . 8
β’ (π’ β π΄ β {π β π΅ β£ π β (πβπ’)} = {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))}) |
49 | 48 | adantl 483 |
. . . . . . 7
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β {π β π΅ β£ π β (πβπ’)} = {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))}) |
50 | 38, 46, 49 | 3eqtr3a 2801 |
. . . . . 6
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (πβπ’) = {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))}) |
51 | | breq2 5114 |
. . . . . . . . . 10
β’ (π¦ = π β (π₯ππ¦ β π₯ππ)) |
52 | 51 | cbvrabv 3420 |
. . . . . . . . 9
β’ {π¦ β π΅ β£ π₯ππ¦} = {π β π΅ β£ π₯ππ} |
53 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ππ β πππ)) |
54 | | df-br 5111 |
. . . . . . . . . . 11
β’ (πππ β β¨π, πβ© β π) |
55 | 53, 54 | bitrdi 287 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ππ β β¨π, πβ© β π)) |
56 | 55 | rabbidv 3418 |
. . . . . . . . 9
β’ (π₯ = π β {π β π΅ β£ π₯ππ} = {π β π΅ β£ β¨π, πβ© β π}) |
57 | 52, 56 | eqtrid 2789 |
. . . . . . . 8
β’ (π₯ = π β {π¦ β π΅ β£ π₯ππ¦} = {π β π΅ β£ β¨π, πβ© β π}) |
58 | 57 | cbvmptv 5223 |
. . . . . . 7
β’ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) = (π β π΄ β¦ {π β π΅ β£ β¨π, πβ© β π}) |
59 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β π = π’) |
60 | 59 | opeq1d 4841 |
. . . . . . . . . 10
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β β¨π, πβ© = β¨π’, πβ©) |
61 | | simpllr 775 |
. . . . . . . . . 10
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
62 | 60, 61 | eleq12d 2832 |
. . . . . . . . 9
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β (β¨π, πβ© β π β β¨π’, πβ© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) |
63 | | vex 3452 |
. . . . . . . . . 10
β’ π’ β V |
64 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
65 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ = π’ β§ π¦ = π) β π₯ = π’) |
66 | 65 | eleq1d 2823 |
. . . . . . . . . . 11
β’ ((π₯ = π’ β§ π¦ = π) β (π₯ β π΄ β π’ β π΄)) |
67 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ = π’ β§ π¦ = π) β π¦ = π) |
68 | 65 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π₯ = π’ β§ π¦ = π) β (πβπ₯) = (πβπ’)) |
69 | 67, 68 | eleq12d 2832 |
. . . . . . . . . . 11
β’ ((π₯ = π’ β§ π¦ = π) β (π¦ β (πβπ₯) β π β (πβπ’))) |
70 | 66, 69 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π₯ = π’ β§ π¦ = π) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β (π’ β π΄ β§ π β (πβπ’)))) |
71 | 63, 64, 70 | opelopaba 5498 |
. . . . . . . . 9
β’
(β¨π’, πβ© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (π’ β π΄ β§ π β (πβπ’))) |
72 | 62, 71 | bitrdi 287 |
. . . . . . . 8
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β (β¨π, πβ© β π β (π’ β π΄ β§ π β (πβπ’)))) |
73 | 72 | rabbidv 3418 |
. . . . . . 7
β’
(((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β§ π = π’) β {π β π΅ β£ β¨π, πβ© β π} = {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))}) |
74 | 2 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β π΅ β π) |
75 | | rabexg 5293 |
. . . . . . . 8
β’ (π΅ β π β {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))} β V) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))} β V) |
77 | 58, 73, 42, 76 | fvmptd2 6961 |
. . . . . 6
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})βπ’) = {π β π΅ β£ (π’ β π΄ β§ π β (πβπ’))}) |
78 | 50, 77 | eqtr4d 2780 |
. . . . 5
β’ ((((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ π’ β π΄) β (πβπ’) = ((π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})βπ’)) |
79 | 31, 37, 78 | eqfnfvd 6990 |
. . . 4
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
80 | | simplrl 776 |
. . . . . . . 8
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β π« (π΄ Γ π΅)) |
81 | 80 | elpwid 4574 |
. . . . . . 7
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (π΄ Γ π΅)) |
82 | | xpss 5654 |
. . . . . . 7
β’ (π΄ Γ π΅) β (V Γ V) |
83 | 81, 82 | sstrdi 3961 |
. . . . . 6
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (V Γ V)) |
84 | | df-rel 5645 |
. . . . . 6
β’ (Rel
π β π β (V Γ V)) |
85 | 83, 84 | sylibr 233 |
. . . . 5
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β Rel π) |
86 | | relopabv 5782 |
. . . . . 6
β’ Rel
{β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} |
87 | 86 | a1i 11 |
. . . . 5
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β Rel {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
88 | | simpl 484 |
. . . . . . 7
β’ ((π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄)) β π β π« (π΄ Γ π΅)) |
89 | 2, 88 | anim12i 614 |
. . . . . 6
β’ ((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β (π΅ β π β§ π β π« (π΄ Γ π΅))) |
90 | 89 | anim1i 616 |
. . . . 5
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
91 | | vex 3452 |
. . . . . . . 8
β’ π£ β V |
92 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ = π’ β§ π¦ = π£) β π₯ = π’) |
93 | 92 | eleq1d 2823 |
. . . . . . . . 9
β’ ((π₯ = π’ β§ π¦ = π£) β (π₯ β π΄ β π’ β π΄)) |
94 | | simpr 486 |
. . . . . . . . . 10
β’ ((π₯ = π’ β§ π¦ = π£) β π¦ = π£) |
95 | 92 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π₯ = π’ β§ π¦ = π£) β (πβπ₯) = (πβπ’)) |
96 | 94, 95 | eleq12d 2832 |
. . . . . . . . 9
β’ ((π₯ = π’ β§ π¦ = π£) β (π¦ β (πβπ₯) β π£ β (πβπ’))) |
97 | 93, 96 | anbi12d 632 |
. . . . . . . 8
β’ ((π₯ = π’ β§ π¦ = π£) β ((π₯ β π΄ β§ π¦ β (πβπ₯)) β (π’ β π΄ β§ π£ β (πβπ’)))) |
98 | 63, 91, 97 | opelopaba 5498 |
. . . . . . 7
β’
(β¨π’, π£β© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β (π’ β π΄ β§ π£ β (πβπ’))) |
99 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = π£ β (π’ππ β π’ππ£)) |
100 | | df-br 5111 |
. . . . . . . . . . . 12
β’ (π’ππ£ β β¨π’, π£β© β π) |
101 | 99, 100 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π = π£ β (π’ππ β β¨π’, π£β© β π)) |
102 | 101 | elrab 3650 |
. . . . . . . . . 10
β’ (π£ β {π β π΅ β£ π’ππ} β (π£ β π΅ β§ β¨π’, π£β© β π)) |
103 | 102 | anbi2i 624 |
. . . . . . . . 9
β’ ((π’ β π΄ β§ π£ β {π β π΅ β£ π’ππ}) β (π’ β π΄ β§ (π£ β π΅ β§ β¨π’, π£β© β π))) |
104 | 103 | a1i 11 |
. . . . . . . 8
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((π’ β π΄ β§ π£ β {π β π΅ β£ π’ππ}) β (π’ β π΄ β§ (π£ β π΅ β§ β¨π’, π£β© β π)))) |
105 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) |
106 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (π₯ππ¦ β πππ¦)) |
107 | 106 | rabbidv 3418 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β {π¦ β π΅ β£ π₯ππ¦} = {π¦ β π΅ β£ πππ¦}) |
108 | | breq2 5114 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (πππ¦ β πππ)) |
109 | 108 | cbvrabv 3420 |
. . . . . . . . . . . . . 14
β’ {π¦ β π΅ β£ πππ¦} = {π β π΅ β£ πππ} |
110 | 107, 109 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π₯ = π β {π¦ β π΅ β£ π₯ππ¦} = {π β π΅ β£ πππ}) |
111 | 110 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}) = (π β π΄ β¦ {π β π΅ β£ πππ}) |
112 | 105, 111 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β π = (π β π΄ β¦ {π β π΅ β£ πππ})) |
113 | | breq1 5113 |
. . . . . . . . . . . . 13
β’ (π = π’ β (πππ β π’ππ)) |
114 | 113 | rabbidv 3418 |
. . . . . . . . . . . 12
β’ (π = π’ β {π β π΅ β£ πππ} = {π β π΅ β£ π’ππ}) |
115 | 114 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β§ π = π’) β {π β π΅ β£ πππ} = {π β π΅ β£ π’ππ}) |
116 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β π’ β π΄) |
117 | | rabexg 5293 |
. . . . . . . . . . . 12
β’ (π΅ β π β {π β π΅ β£ π’ππ} β V) |
118 | 117 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β {π β π΅ β£ π’ππ} β V) |
119 | 112, 115,
116, 118 | fvmptd 6960 |
. . . . . . . . . 10
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β (πβπ’) = {π β π΅ β£ π’ππ}) |
120 | 119 | eleq2d 2824 |
. . . . . . . . 9
β’ ((((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β§ π’ β π΄) β (π£ β (πβπ’) β π£ β {π β π΅ β£ π’ππ})) |
121 | 120 | pm5.32da 580 |
. . . . . . . 8
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((π’ β π΄ β§ π£ β (πβπ’)) β (π’ β π΄ β§ π£ β {π β π΅ β£ π’ππ}))) |
122 | | simplr 768 |
. . . . . . . . . 10
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β π« (π΄ Γ π΅)) |
123 | 122 | elpwid 4574 |
. . . . . . . . 9
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π β (π΄ Γ π΅)) |
124 | 63, 91 | opeldm 5868 |
. . . . . . . . . . . 12
β’
(β¨π’, π£β© β π β π’ β dom π) |
125 | | dmss 5863 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ Γ π΅) β dom π β dom (π΄ Γ π΅)) |
126 | | dmxpss 6128 |
. . . . . . . . . . . . . 14
β’ dom
(π΄ Γ π΅) β π΄ |
127 | 125, 126 | sstrdi 3961 |
. . . . . . . . . . . . 13
β’ (π β (π΄ Γ π΅) β dom π β π΄) |
128 | 127 | sseld 3948 |
. . . . . . . . . . . 12
β’ (π β (π΄ Γ π΅) β (π’ β dom π β π’ β π΄)) |
129 | 124, 128 | syl5 34 |
. . . . . . . . . . 11
β’ (π β (π΄ Γ π΅) β (β¨π’, π£β© β π β π’ β π΄)) |
130 | 129 | pm4.71rd 564 |
. . . . . . . . . 10
β’ (π β (π΄ Γ π΅) β (β¨π’, π£β© β π β (π’ β π΄ β§ β¨π’, π£β© β π))) |
131 | 63, 91 | opelrn 5903 |
. . . . . . . . . . . . 13
β’
(β¨π’, π£β© β π β π£ β ran π) |
132 | | rnss 5899 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ Γ π΅) β ran π β ran (π΄ Γ π΅)) |
133 | | rnxpss 6129 |
. . . . . . . . . . . . . . 15
β’ ran
(π΄ Γ π΅) β π΅ |
134 | 132, 133 | sstrdi 3961 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ Γ π΅) β ran π β π΅) |
135 | 134 | sseld 3948 |
. . . . . . . . . . . . 13
β’ (π β (π΄ Γ π΅) β (π£ β ran π β π£ β π΅)) |
136 | 131, 135 | syl5 34 |
. . . . . . . . . . . 12
β’ (π β (π΄ Γ π΅) β (β¨π’, π£β© β π β π£ β π΅)) |
137 | 136 | pm4.71rd 564 |
. . . . . . . . . . 11
β’ (π β (π΄ Γ π΅) β (β¨π’, π£β© β π β (π£ β π΅ β§ β¨π’, π£β© β π))) |
138 | 137 | anbi2d 630 |
. . . . . . . . . 10
β’ (π β (π΄ Γ π΅) β ((π’ β π΄ β§ β¨π’, π£β© β π) β (π’ β π΄ β§ (π£ β π΅ β§ β¨π’, π£β© β π)))) |
139 | 130, 138 | bitrd 279 |
. . . . . . . . 9
β’ (π β (π΄ Γ π΅) β (β¨π’, π£β© β π β (π’ β π΄ β§ (π£ β π΅ β§ β¨π’, π£β© β π)))) |
140 | 123, 139 | syl 17 |
. . . . . . . 8
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (β¨π’, π£β© β π β (π’ β π΄ β§ (π£ β π΅ β§ β¨π’, π£β© β π)))) |
141 | 104, 121,
140 | 3bitr4d 311 |
. . . . . . 7
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((π’ β π΄ β§ π£ β (πβπ’)) β β¨π’, π£β© β π)) |
142 | 98, 141 | bitr2id 284 |
. . . . . 6
β’ (((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (β¨π’, π£β© β π β β¨π’, π£β© β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) |
143 | 142 | eqrelrdv2 5756 |
. . . . 5
β’ (((Rel
π β§ Rel {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β§ ((π΅ β π β§ π β π« (π΄ Γ π΅)) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
144 | 85, 87, 90, 143 | syl21anc 837 |
. . . 4
β’ (((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β§ π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) |
145 | 79, 144 | impbida 800 |
. . 3
β’ ((π β§ (π β π« (π΄ Γ π΅) β§ π β (π« π΅ βm π΄))) β (π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))} β π = (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
146 | 1, 12, 28, 145 | f1ocnv2d 7611 |
. 2
β’ (π β ((π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})):π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘(π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}))) |
147 | | rfovcnvf1od.f |
. . . 4
β’ πΉ = (π΄ππ΅) |
148 | | rfovd.rf |
. . . . 5
β’ π = (π β V, π β V β¦ (π β π« (π Γ π) β¦ (π₯ β π β¦ {π¦ β π β£ π₯ππ¦}))) |
149 | 148, 9, 2 | rfovd 42347 |
. . . 4
β’ (π β (π΄ππ΅) = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
150 | 147, 149 | eqtrid 2789 |
. . 3
β’ (π β πΉ = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
151 | | f1oeq1 6777 |
. . . 4
β’ (πΉ = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (πΉ:π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})):π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄))) |
152 | | cnveq 5834 |
. . . . 5
β’ (πΉ = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β β‘πΉ = β‘(π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦}))) |
153 | 152 | eqeq1d 2739 |
. . . 4
β’ (πΉ = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β (β‘πΉ = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β β‘(π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}))) |
154 | 151, 153 | anbi12d 632 |
. . 3
β’ (πΉ = (π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) β ((πΉ:π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘πΉ = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) β ((π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})):π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘(π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})))) |
155 | 150, 154 | syl 17 |
. 2
β’ (π β ((πΉ:π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘πΉ = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})) β ((π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})):π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘(π β π« (π΄ Γ π΅) β¦ (π₯ β π΄ β¦ {π¦ β π΅ β£ π₯ππ¦})) = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))})))) |
156 | 146, 155 | mpbird 257 |
1
β’ (π β (πΉ:π« (π΄ Γ π΅)β1-1-ontoβ(π« π΅ βm π΄) β§ β‘πΉ = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}))) |