Step | Hyp | Ref
| Expression |
1 | | fsovd.b |
. . . . . 6
β’ (π β π΅ β π) |
2 | | fsovd.a |
. . . . . 6
β’ (π β π΄ β π) |
3 | 1, 2 | xpexd 7690 |
. . . . 5
β’ (π β (π΅ Γ π΄) β V) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π β (π« π΅ βm π΄)) β (π΅ Γ π΄) β V) |
5 | | elmapi 8794 |
. . . . . . . . . . . . . . 15
β’ (π β (π« π΅ βm π΄) β π:π΄βΆπ« π΅) |
6 | 5 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((π β (π« π΅ βm π΄) β§ π’ β π΄) β (πβπ’) β π« π΅) |
7 | 6 | elpwid 4574 |
. . . . . . . . . . . . 13
β’ ((π β (π« π΅ βm π΄) β§ π’ β π΄) β (πβπ’) β π΅) |
8 | 7 | sseld 3948 |
. . . . . . . . . . . 12
β’ ((π β (π« π΅ βm π΄) β§ π’ β π΄) β (π£ β (πβπ’) β π£ β π΅)) |
9 | 8 | impancom 453 |
. . . . . . . . . . 11
β’ ((π β (π« π΅ βm π΄) β§ π£ β (πβπ’)) β (π’ β π΄ β π£ β π΅)) |
10 | 9 | pm4.71d 563 |
. . . . . . . . . 10
β’ ((π β (π« π΅ βm π΄) β§ π£ β (πβπ’)) β (π’ β π΄ β (π’ β π΄ β§ π£ β π΅))) |
11 | 10 | ex 414 |
. . . . . . . . 9
β’ (π β (π« π΅ βm π΄) β (π£ β (πβπ’) β (π’ β π΄ β (π’ β π΄ β§ π£ β π΅)))) |
12 | 11 | pm5.32rd 579 |
. . . . . . . 8
β’ (π β (π« π΅ βm π΄) β ((π’ β π΄ β§ π£ β (πβπ’)) β ((π’ β π΄ β§ π£ β π΅) β§ π£ β (πβπ’)))) |
13 | | ancom 462 |
. . . . . . . . 9
β’ ((π’ β π΄ β§ π£ β π΅) β (π£ β π΅ β§ π’ β π΄)) |
14 | 13 | anbi1i 625 |
. . . . . . . 8
β’ (((π’ β π΄ β§ π£ β π΅) β§ π£ β (πβπ’)) β ((π£ β π΅ β§ π’ β π΄) β§ π£ β (πβπ’))) |
15 | 12, 14 | bitrdi 287 |
. . . . . . 7
β’ (π β (π« π΅ βm π΄) β ((π’ β π΄ β§ π£ β (πβπ’)) β ((π£ β π΅ β§ π’ β π΄) β§ π£ β (πβπ’)))) |
16 | 15 | opabbidv 5176 |
. . . . . 6
β’ (π β (π« π΅ βm π΄) β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} = {β¨π£, π’β© β£ ((π£ β π΅ β§ π’ β π΄) β§ π£ β (πβπ’))}) |
17 | | opabssxp 5729 |
. . . . . 6
β’
{β¨π£, π’β© β£ ((π£ β π΅ β§ π’ β π΄) β§ π£ β (πβπ’))} β (π΅ Γ π΄) |
18 | 16, 17 | eqsstrdi 4003 |
. . . . 5
β’ (π β (π« π΅ βm π΄) β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π΅ Γ π΄)) |
19 | 18 | adantl 483 |
. . . 4
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π΅ Γ π΄)) |
20 | 4, 19 | sselpwd 5288 |
. . 3
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β π« (π΅ Γ π΄)) |
21 | | eqidd 2738 |
. . 3
β’ (π β (π β (π« π΅ βm π΄) β¦ {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}) = (π β (π« π΅ βm π΄) β¦ {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))})) |
22 | | fsovd.rf |
. . . . 5
β’ π
= (π β V, π β V β¦ (π β π« (π Γ π) β¦ (π’ β π β¦ {π£ β π β£ π’ππ£}))) |
23 | 22, 1, 2 | rfovd 42347 |
. . . 4
β’ (π β (π΅π
π΄) = (π β π« (π΅ Γ π΄) β¦ (π’ β π΅ β¦ {π£ β π΄ β£ π’ππ£}))) |
24 | | breq 5112 |
. . . . . . . 8
β’ (π = π‘ β (π’ππ£ β π’π‘π£)) |
25 | 24 | rabbidv 3418 |
. . . . . . 7
β’ (π = π‘ β {π£ β π΄ β£ π’ππ£} = {π£ β π΄ β£ π’π‘π£}) |
26 | 25 | mpteq2dv 5212 |
. . . . . 6
β’ (π = π‘ β (π’ β π΅ β¦ {π£ β π΄ β£ π’ππ£}) = (π’ β π΅ β¦ {π£ β π΄ β£ π’π‘π£})) |
27 | | breq1 5113 |
. . . . . . . . 9
β’ (π’ = π β (π’π‘π£ β ππ‘π£)) |
28 | 27 | rabbidv 3418 |
. . . . . . . 8
β’ (π’ = π β {π£ β π΄ β£ π’π‘π£} = {π£ β π΄ β£ ππ‘π£}) |
29 | | breq2 5114 |
. . . . . . . . 9
β’ (π£ = π β (ππ‘π£ β ππ‘π)) |
30 | 29 | cbvrabv 3420 |
. . . . . . . 8
β’ {π£ β π΄ β£ ππ‘π£} = {π β π΄ β£ ππ‘π} |
31 | 28, 30 | eqtrdi 2793 |
. . . . . . 7
β’ (π’ = π β {π£ β π΄ β£ π’π‘π£} = {π β π΄ β£ ππ‘π}) |
32 | 31 | cbvmptv 5223 |
. . . . . 6
β’ (π’ β π΅ β¦ {π£ β π΄ β£ π’π‘π£}) = (π β π΅ β¦ {π β π΄ β£ ππ‘π}) |
33 | 26, 32 | eqtrdi 2793 |
. . . . 5
β’ (π = π‘ β (π’ β π΅ β¦ {π£ β π΄ β£ π’ππ£}) = (π β π΅ β¦ {π β π΄ β£ ππ‘π})) |
34 | 33 | cbvmptv 5223 |
. . . 4
β’ (π β π« (π΅ Γ π΄) β¦ (π’ β π΅ β¦ {π£ β π΄ β£ π’ππ£})) = (π‘ β π« (π΅ Γ π΄) β¦ (π β π΅ β¦ {π β π΄ β£ ππ‘π})) |
35 | 23, 34 | eqtrdi 2793 |
. . 3
β’ (π β (π΅π
π΄) = (π‘ β π« (π΅ Γ π΄) β¦ (π β π΅ β¦ {π β π΄ β£ ππ‘π}))) |
36 | | breq 5112 |
. . . . . . 7
β’ (π‘ = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (ππ‘π β π{β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}π)) |
37 | | df-br 5111 |
. . . . . . . 8
β’ (π{β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}π β β¨π, πβ© β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}) |
38 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
39 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
40 | | eleq1w 2821 |
. . . . . . . . . 10
β’ (π£ = π β (π£ β (πβπ’) β π β (πβπ’))) |
41 | 40 | anbi2d 630 |
. . . . . . . . 9
β’ (π£ = π β ((π’ β π΄ β§ π£ β (πβπ’)) β (π’ β π΄ β§ π β (πβπ’)))) |
42 | | eleq1w 2821 |
. . . . . . . . . 10
β’ (π’ = π β (π’ β π΄ β π β π΄)) |
43 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π’ = π β (πβπ’) = (πβπ)) |
44 | 43 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π’ = π β (π β (πβπ’) β π β (πβπ))) |
45 | 42, 44 | anbi12d 632 |
. . . . . . . . 9
β’ (π’ = π β ((π’ β π΄ β§ π β (πβπ’)) β (π β π΄ β§ π β (πβπ)))) |
46 | 38, 39, 41, 45 | opelopab 5504 |
. . . . . . . 8
β’
(β¨π, πβ© β {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π β π΄ β§ π β (πβπ))) |
47 | 37, 46 | bitri 275 |
. . . . . . 7
β’ (π{β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}π β (π β π΄ β§ π β (πβπ))) |
48 | 36, 47 | bitrdi 287 |
. . . . . 6
β’ (π‘ = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (ππ‘π β (π β π΄ β§ π β (πβπ)))) |
49 | 48 | rabbidv 3418 |
. . . . 5
β’ (π‘ = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β {π β π΄ β£ ππ‘π} = {π β π΄ β£ (π β π΄ β§ π β (πβπ))}) |
50 | 49 | mpteq2dv 5212 |
. . . 4
β’ (π‘ = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π β π΅ β¦ {π β π΄ β£ ππ‘π}) = (π β π΅ β¦ {π β π΄ β£ (π β π΄ β§ π β (πβπ))})) |
51 | | ibar 530 |
. . . . . . . . 9
β’ (π β π΄ β (π β (πβπ) β (π β π΄ β§ π β (πβπ)))) |
52 | 51 | bicomd 222 |
. . . . . . . 8
β’ (π β π΄ β ((π β π΄ β§ π β (πβπ)) β π β (πβπ))) |
53 | 52 | rabbiia 3414 |
. . . . . . 7
β’ {π β π΄ β£ (π β π΄ β§ π β (πβπ))} = {π β π΄ β£ π β (πβπ)} |
54 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
55 | 54 | eleq2d 2824 |
. . . . . . . 8
β’ (π = π₯ β (π β (πβπ) β π β (πβπ₯))) |
56 | 55 | cbvrabv 3420 |
. . . . . . 7
β’ {π β π΄ β£ π β (πβπ)} = {π₯ β π΄ β£ π β (πβπ₯)} |
57 | 53, 56 | eqtri 2765 |
. . . . . 6
β’ {π β π΄ β£ (π β π΄ β§ π β (πβπ))} = {π₯ β π΄ β£ π β (πβπ₯)} |
58 | 57 | mpteq2i 5215 |
. . . . 5
β’ (π β π΅ β¦ {π β π΄ β£ (π β π΄ β§ π β (πβπ))}) = (π β π΅ β¦ {π₯ β π΄ β£ π β (πβπ₯)}) |
59 | | eleq1w 2821 |
. . . . . . 7
β’ (π = π¦ β (π β (πβπ₯) β π¦ β (πβπ₯))) |
60 | 59 | rabbidv 3418 |
. . . . . 6
β’ (π = π¦ β {π₯ β π΄ β£ π β (πβπ₯)} = {π₯ β π΄ β£ π¦ β (πβπ₯)}) |
61 | 60 | cbvmptv 5223 |
. . . . 5
β’ (π β π΅ β¦ {π₯ β π΄ β£ π β (πβπ₯)}) = (π¦ β π΅ β¦ {π₯ β π΄ β£ π¦ β (πβπ₯)}) |
62 | 58, 61 | eqtri 2765 |
. . . 4
β’ (π β π΅ β¦ {π β π΄ β£ (π β π΄ β§ π β (πβπ))}) = (π¦ β π΅ β¦ {π₯ β π΄ β£ π¦ β (πβπ₯)}) |
63 | 50, 62 | eqtrdi 2793 |
. . 3
β’ (π‘ = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π β π΅ β¦ {π β π΄ β£ ππ‘π}) = (π¦ β π΅ β¦ {π₯ β π΄ β£ π¦ β (πβπ₯)})) |
64 | 20, 21, 35, 63 | fmptco 7080 |
. 2
β’ (π β ((π΅π
π΄) β (π β (π« π΅ βm π΄) β¦ {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))})) = (π β (π« π΅ βm π΄) β¦ (π¦ β π΅ β¦ {π₯ β π΄ β£ π¦ β (πβπ₯)}))) |
65 | 2, 1 | xpexd 7690 |
. . . . . 6
β’ (π β (π΄ Γ π΅) β V) |
66 | 65 | adantr 482 |
. . . . 5
β’ ((π β§ π β (π« π΅ βm π΄)) β (π΄ Γ π΅) β V) |
67 | 12 | opabbidv 5176 |
. . . . . . 7
β’ (π β (π« π΅ βm π΄) β {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} = {β¨π’, π£β© β£ ((π’ β π΄ β§ π£ β π΅) β§ π£ β (πβπ’))}) |
68 | | opabssxp 5729 |
. . . . . . 7
β’
{β¨π’, π£β© β£ ((π’ β π΄ β§ π£ β π΅) β§ π£ β (πβπ’))} β (π΄ Γ π΅) |
69 | 67, 68 | eqsstrdi 4003 |
. . . . . 6
β’ (π β (π« π΅ βm π΄) β {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π΄ Γ π΅)) |
70 | 69 | adantl 483 |
. . . . 5
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β (π΄ Γ π΅)) |
71 | 66, 70 | sselpwd 5288 |
. . . 4
β’ ((π β§ π β (π« π΅ βm π΄)) β {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β π« (π΄ Γ π΅)) |
72 | | eqid 2737 |
. . . . 5
β’ (π΄π
π΅) = (π΄π
π΅) |
73 | 22, 2, 1, 72 | rfovcnvd 42351 |
. . . 4
β’ (π β β‘(π΄π
π΅) = (π β (π« π΅ βm π΄) β¦ {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))})) |
74 | | fsovd.cnv |
. . . . . 6
β’ πΆ = (π β V, π β V β¦ (π β π« (π Γ π) β¦ β‘π )) |
75 | 74 | a1i 11 |
. . . . 5
β’ (π β πΆ = (π β V, π β V β¦ (π β π« (π Γ π) β¦ β‘π ))) |
76 | | xpeq12 5663 |
. . . . . . . 8
β’ ((π = π΄ β§ π = π΅) β (π Γ π) = (π΄ Γ π΅)) |
77 | 76 | pweqd 4582 |
. . . . . . 7
β’ ((π = π΄ β§ π = π΅) β π« (π Γ π) = π« (π΄ Γ π΅)) |
78 | 77 | mpteq1d 5205 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β (π β π« (π Γ π) β¦ β‘π ) = (π β π« (π΄ Γ π΅) β¦ β‘π )) |
79 | 78 | adantl 483 |
. . . . 5
β’ ((π β§ (π = π΄ β§ π = π΅)) β (π β π« (π Γ π) β¦ β‘π ) = (π β π« (π΄ Γ π΅) β¦ β‘π )) |
80 | 2 | elexd 3468 |
. . . . 5
β’ (π β π΄ β V) |
81 | 1 | elexd 3468 |
. . . . 5
β’ (π β π΅ β V) |
82 | | pwexg 5338 |
. . . . . 6
β’ ((π΄ Γ π΅) β V β π« (π΄ Γ π΅) β V) |
83 | | mptexg 7176 |
. . . . . 6
β’
(π« (π΄
Γ π΅) β V β
(π β π« (π΄ Γ π΅) β¦ β‘π ) β V) |
84 | 65, 82, 83 | 3syl 18 |
. . . . 5
β’ (π β (π β π« (π΄ Γ π΅) β¦ β‘π ) β V) |
85 | 75, 79, 80, 81, 84 | ovmpod 7512 |
. . . 4
β’ (π β (π΄πΆπ΅) = (π β π« (π΄ Γ π΅) β¦ β‘π )) |
86 | | cnveq 5834 |
. . . . 5
β’ (π = {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β β‘π = β‘{β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))}) |
87 | | cnvopab 6096 |
. . . . 5
β’ β‘{β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))} |
88 | 86, 87 | eqtrdi 2793 |
. . . 4
β’ (π = {β¨π’, π£β© β£ (π’ β π΄ β§ π£ β (πβπ’))} β β‘π = {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}) |
89 | 71, 73, 85, 88 | fmptco 7080 |
. . 3
β’ (π β ((π΄πΆπ΅) β β‘(π΄π
π΅)) = (π β (π« π΅ βm π΄) β¦ {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))})) |
90 | 89 | coeq2d 5823 |
. 2
β’ (π β ((π΅π
π΄) β ((π΄πΆπ΅) β β‘(π΄π
π΅))) = ((π΅π
π΄) β (π β (π« π΅ βm π΄) β¦ {β¨π£, π’β© β£ (π’ β π΄ β§ π£ β (πβπ’))}))) |
91 | | fsovd.fs |
. . 3
β’ π = (π β V, π β V β¦ (π β (π« π βm π) β¦ (π¦ β π β¦ {π₯ β π β£ π¦ β (πβπ₯)}))) |
92 | 91, 2, 1 | fsovd 42354 |
. 2
β’ (π β (π΄ππ΅) = (π β (π« π΅ βm π΄) β¦ (π¦ β π΅ β¦ {π₯ β π΄ β£ π¦ β (πβπ₯)}))) |
93 | 64, 90, 92 | 3eqtr4rd 2788 |
1
β’ (π β (π΄ππ΅) = ((π΅π
π΄) β ((π΄πΆπ΅) β β‘(π΄π
π΅)))) |