Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fsovrfovd Structured version   Visualization version   GIF version

Theorem fsovrfovd 42355
Description: The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021.)
Hypotheses
Ref Expression
fsovd.fs 𝑂 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m π‘Ž) ↦ (𝑦 ∈ 𝑏 ↦ {π‘₯ ∈ π‘Ž ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
fsovd.a (πœ‘ β†’ 𝐴 ∈ 𝑉)
fsovd.b (πœ‘ β†’ 𝐡 ∈ π‘Š)
fsovd.rf 𝑅 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ (𝑒 ∈ π‘Ž ↦ {𝑣 ∈ 𝑏 ∣ π‘’π‘Ÿπ‘£})))
fsovd.cnv 𝐢 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠))
Assertion
Ref Expression
fsovrfovd (πœ‘ β†’ (𝐴𝑂𝐡) = ((𝐡𝑅𝐴) ∘ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡))))
Distinct variable groups:   𝐴,π‘Ž,𝑏,𝑓,π‘Ÿ,𝑒,𝑣   𝐴,𝑠,π‘Ž,𝑏,𝑓,𝑒,𝑣   π‘₯,𝐴,𝑦,π‘Ž,𝑏,𝑓   𝐡,π‘Ž,𝑏,𝑓,π‘Ÿ,𝑒,𝑣   𝐡,𝑠   𝑦,𝐡   π‘Š,π‘Ž,𝑒   πœ‘,π‘Ž,𝑏,𝑓,π‘Ÿ,𝑒,𝑣
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑠)   𝐡(π‘₯)   𝐢(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑠,π‘Ÿ,π‘Ž,𝑏)   𝑅(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑠,π‘Ÿ,π‘Ž,𝑏)   𝑂(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑠,π‘Ÿ,π‘Ž,𝑏)   𝑉(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑠,π‘Ÿ,π‘Ž,𝑏)   π‘Š(π‘₯,𝑦,𝑣,𝑓,𝑠,π‘Ÿ,𝑏)

Proof of Theorem fsovrfovd
Dummy variables 𝑐 𝑑 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsovd.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ π‘Š)
2 fsovd.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑉)
31, 2xpexd 7690 . . . . 5 (πœ‘ β†’ (𝐡 Γ— 𝐴) ∈ V)
43adantr 482 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (𝐡 Γ— 𝐴) ∈ V)
5 elmapi 8794 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ 𝑓:π΄βŸΆπ’« 𝐡)
65ffvelcdmda 7040 . . . . . . . . . . . . . 14 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) ∈ 𝒫 𝐡)
76elpwid 4574 . . . . . . . . . . . . 13 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) βŠ† 𝐡)
87sseld 3948 . . . . . . . . . . . 12 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ (π‘“β€˜π‘’) β†’ 𝑣 ∈ 𝐡))
98impancom 453 . . . . . . . . . . 11 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) β†’ (𝑒 ∈ 𝐴 β†’ 𝑣 ∈ 𝐡))
109pm4.71d 563 . . . . . . . . . 10 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) β†’ (𝑒 ∈ 𝐴 ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡)))
1110ex 414 . . . . . . . . 9 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ (𝑣 ∈ (π‘“β€˜π‘’) β†’ (𝑒 ∈ 𝐴 ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡))))
1211pm5.32rd 579 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))))
13 ancom 462 . . . . . . . . 9 ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ↔ (𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴))
1413anbi1i 625 . . . . . . . 8 (((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)))
1512, 14bitrdi 287 . . . . . . 7 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))))
1615opabbidv 5176 . . . . . 6 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘£, π‘’βŸ© ∣ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
17 opabssxp 5729 . . . . . 6 {βŸ¨π‘£, π‘’βŸ© ∣ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴)
1816, 17eqsstrdi 4003 . . . . 5 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴))
1918adantl 483 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴))
204, 19sselpwd 5288 . . 3 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ∈ 𝒫 (𝐡 Γ— 𝐴))
21 eqidd 2738 . . 3 (πœ‘ β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
22 fsovd.rf . . . . 5 𝑅 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ (𝑒 ∈ π‘Ž ↦ {𝑣 ∈ 𝑏 ∣ π‘’π‘Ÿπ‘£})))
2322, 1, 2rfovd 42347 . . . 4 (πœ‘ β†’ (𝐡𝑅𝐴) = (π‘Ÿ ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£})))
24 breq 5112 . . . . . . . 8 (π‘Ÿ = 𝑑 β†’ (π‘’π‘Ÿπ‘£ ↔ 𝑒𝑑𝑣))
2524rabbidv 3418 . . . . . . 7 (π‘Ÿ = 𝑑 β†’ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£} = {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣})
2625mpteq2dv 5212 . . . . . 6 (π‘Ÿ = 𝑑 β†’ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£}) = (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣}))
27 breq1 5113 . . . . . . . . 9 (𝑒 = 𝑐 β†’ (𝑒𝑑𝑣 ↔ 𝑐𝑑𝑣))
2827rabbidv 3418 . . . . . . . 8 (𝑒 = 𝑐 β†’ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑑𝑣})
29 breq2 5114 . . . . . . . . 9 (𝑣 = 𝑑 β†’ (𝑐𝑑𝑣 ↔ 𝑐𝑑𝑑))
3029cbvrabv 3420 . . . . . . . 8 {𝑣 ∈ 𝐴 ∣ 𝑐𝑑𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}
3128, 30eqtrdi 2793 . . . . . . 7 (𝑒 = 𝑐 β†’ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑})
3231cbvmptv 5223 . . . . . 6 (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑})
3326, 32eqtrdi 2793 . . . . 5 (π‘Ÿ = 𝑑 β†’ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}))
3433cbvmptv 5223 . . . 4 (π‘Ÿ ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£})) = (𝑑 ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}))
3523, 34eqtrdi 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 (𝑣 = 𝑐 β†’ (𝑣 ∈ (π‘“β€˜π‘’) ↔ 𝑐 ∈ (π‘“β€˜π‘’)))
4140anbi2d 630 . . . . . . . . 9 (𝑣 = 𝑐 β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ (𝑒 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘’))))
42 eleq1w 2821 . . . . . . . . . 10 (𝑒 = 𝑑 β†’ (𝑒 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
43 fveq2 6847 . . . . . . . . . . 11 (𝑒 = 𝑑 β†’ (π‘“β€˜π‘’) = (π‘“β€˜π‘‘))
4443eleq2d 2824 . . . . . . . . . 10 (𝑒 = 𝑑 β†’ (𝑐 ∈ (π‘“β€˜π‘’) ↔ 𝑐 ∈ (π‘“β€˜π‘‘)))
4542, 44anbi12d 632 . . . . . . . . 9 (𝑒 = 𝑑 β†’ ((𝑒 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘’)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
4638, 39, 41, 45opelopab 5504 . . . . . . . 8 (βŸ¨π‘, π‘‘βŸ© ∈ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)))
4737, 46bitri 275 . . . . . . 7 (𝑐{βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)))
4836, 47bitrdi 287 . . . . . 6 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐𝑑𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
4948rabbidv 3418 . . . . 5 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))})
5049mpteq2dv 5212 . . . 4 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}))
51 ibar 530 . . . . . . . . 9 (𝑑 ∈ 𝐴 β†’ (𝑐 ∈ (π‘“β€˜π‘‘) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
5251bicomd 222 . . . . . . . 8 (𝑑 ∈ 𝐴 β†’ ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)) ↔ 𝑐 ∈ (π‘“β€˜π‘‘)))
5352rabbiia 3414 . . . . . . 7 {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘‘)}
54 fveq2 6847 . . . . . . . . 9 (𝑑 = π‘₯ β†’ (π‘“β€˜π‘‘) = (π‘“β€˜π‘₯))
5554eleq2d 2824 . . . . . . . 8 (𝑑 = π‘₯ β†’ (𝑐 ∈ (π‘“β€˜π‘‘) ↔ 𝑐 ∈ (π‘“β€˜π‘₯)))
5655cbvrabv 3420 . . . . . . 7 {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘‘)} = {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}
5753, 56eqtri 2765 . . . . . 6 {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))} = {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}
5857mpteq2i 5215 . . . . 5 (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}) = (𝑐 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)})
59 eleq1w 2821 . . . . . . 7 (𝑐 = 𝑦 β†’ (𝑐 ∈ (π‘“β€˜π‘₯) ↔ 𝑦 ∈ (π‘“β€˜π‘₯)))
6059rabbidv 3418 . . . . . 6 (𝑐 = 𝑦 β†’ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)} = {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6160cbvmptv 5223 . . . . 5 (𝑐 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6258, 61eqtri 2765 . . . 4 (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6350, 62eqtrdi 2793 . . 3 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)}))
6420, 21, 35, 63fmptco 7080 . 2 (πœ‘ β†’ ((𝐡𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
652, 1xpexd 7690 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— 𝐡) ∈ V)
6665adantr 482 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (𝐴 Γ— 𝐡) ∈ V)
6712opabbidv 5176 . . . . . . 7 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
68 opabssxp 5729 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡)
6967, 68eqsstrdi 4003 . . . . . 6 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡))
7069adantl 483 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡))
7166, 70sselpwd 5288 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ∈ 𝒫 (𝐴 Γ— 𝐡))
72 eqid 2737 . . . . 5 (𝐴𝑅𝐡) = (𝐴𝑅𝐡)
7322, 2, 1, 72rfovcnvd 42351 . . . 4 (πœ‘ β†’ β—‘(𝐴𝑅𝐡) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
74 fsovd.cnv . . . . . 6 𝐢 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠))
7574a1i 11 . . . . 5 (πœ‘ β†’ 𝐢 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠)))
76 xpeq12 5663 . . . . . . . 8 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (π‘Ž Γ— 𝑏) = (𝐴 Γ— 𝐡))
7776pweqd 4582 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ 𝒫 (π‘Ž Γ— 𝑏) = 𝒫 (𝐴 Γ— 𝐡))
7877mpteq1d 5205 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
7978adantl 483 . . . . 5 ((πœ‘ ∧ (π‘Ž = 𝐴 ∧ 𝑏 = 𝐡)) β†’ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
802elexd 3468 . . . . 5 (πœ‘ β†’ 𝐴 ∈ V)
811elexd 3468 . . . . 5 (πœ‘ β†’ 𝐡 ∈ V)
82 pwexg 5338 . . . . . 6 ((𝐴 Γ— 𝐡) ∈ V β†’ 𝒫 (𝐴 Γ— 𝐡) ∈ V)
83 mptexg 7176 . . . . . 6 (𝒫 (𝐴 Γ— 𝐡) ∈ V β†’ (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠) ∈ V)
8465, 82, 833syl 18 . . . . 5 (πœ‘ β†’ (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠) ∈ V)
8575, 79, 80, 81, 84ovmpod 7512 . . . 4 (πœ‘ β†’ (𝐴𝐢𝐡) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
86 cnveq 5834 . . . . 5 (𝑠 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ ◑𝑠 = β—‘{βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
87 cnvopab 6096 . . . . 5 β—‘{βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}
8886, 87eqtrdi 2793 . . . 4 (𝑠 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ ◑𝑠 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
8971, 73, 85, 88fmptco 7080 . . 3 (πœ‘ β†’ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡)) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
9089coeq2d 5823 . 2 (πœ‘ β†’ ((𝐡𝑅𝐴) ∘ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡))) = ((𝐡𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})))
91 fsovd.fs . . 3 𝑂 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m π‘Ž) ↦ (𝑦 ∈ 𝑏 ↦ {π‘₯ ∈ π‘Ž ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
9291, 2, 1fsovd 42354 . 2 (πœ‘ β†’ (𝐴𝑂𝐡) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
9364, 90, 923eqtr4rd 2788 1 (πœ‘ β†’ (𝐴𝑂𝐡) = ((𝐡𝑅𝐴) ∘ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3410  Vcvv 3448   βŠ† wss 3915  π’« cpw 4565  βŸ¨cop 4597   class class class wbr 5110  {copab 5172   ↦ cmpt 5193   Γ— cxp 5636  β—‘ccnv 5637   ∘ ccom 5642  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364   ↑m cmap 8772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-map 8774
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator