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 42842
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 7740 . . . . 5 (πœ‘ β†’ (𝐡 Γ— 𝐴) ∈ V)
43adantr 481 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (𝐡 Γ— 𝐴) ∈ V)
5 elmapi 8845 . . . . . . . . . . . . . . 15 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ 𝑓:π΄βŸΆπ’« 𝐡)
65ffvelcdmda 7086 . . . . . . . . . . . . . 14 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) ∈ 𝒫 𝐡)
76elpwid 4611 . . . . . . . . . . . . 13 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) βŠ† 𝐡)
87sseld 3981 . . . . . . . . . . . 12 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ (π‘“β€˜π‘’) β†’ 𝑣 ∈ 𝐡))
98impancom 452 . . . . . . . . . . 11 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) β†’ (𝑒 ∈ 𝐴 β†’ 𝑣 ∈ 𝐡))
109pm4.71d 562 . . . . . . . . . 10 ((𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) β†’ (𝑒 ∈ 𝐴 ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡)))
1110ex 413 . . . . . . . . 9 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ (𝑣 ∈ (π‘“β€˜π‘’) β†’ (𝑒 ∈ 𝐴 ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡))))
1211pm5.32rd 578 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))))
13 ancom 461 . . . . . . . . 9 ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ↔ (𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴))
1413anbi1i 624 . . . . . . . 8 (((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’)))
1512, 14bitrdi 286 . . . . . . 7 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))))
1615opabbidv 5214 . . . . . 6 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘£, π‘’βŸ© ∣ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
17 opabssxp 5768 . . . . . 6 {βŸ¨π‘£, π‘’βŸ© ∣ ((𝑣 ∈ 𝐡 ∧ 𝑒 ∈ 𝐴) ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴)
1816, 17eqsstrdi 4036 . . . . 5 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴))
1918adantl 482 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐡 Γ— 𝐴))
204, 19sselpwd 5326 . . 3 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ∈ 𝒫 (𝐡 Γ— 𝐴))
21 eqidd 2733 . . 3 (πœ‘ β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
22 fsovd.rf . . . . 5 𝑅 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ (𝑒 ∈ π‘Ž ↦ {𝑣 ∈ 𝑏 ∣ π‘’π‘Ÿπ‘£})))
2322, 1, 2rfovd 42834 . . . 4 (πœ‘ β†’ (𝐡𝑅𝐴) = (π‘Ÿ ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£})))
24 breq 5150 . . . . . . . 8 (π‘Ÿ = 𝑑 β†’ (π‘’π‘Ÿπ‘£ ↔ 𝑒𝑑𝑣))
2524rabbidv 3440 . . . . . . 7 (π‘Ÿ = 𝑑 β†’ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£} = {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣})
2625mpteq2dv 5250 . . . . . 6 (π‘Ÿ = 𝑑 β†’ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£}) = (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣}))
27 breq1 5151 . . . . . . . . 9 (𝑒 = 𝑐 β†’ (𝑒𝑑𝑣 ↔ 𝑐𝑑𝑣))
2827rabbidv 3440 . . . . . . . 8 (𝑒 = 𝑐 β†’ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣} = {𝑣 ∈ 𝐴 ∣ 𝑐𝑑𝑣})
29 breq2 5152 . . . . . . . . 9 (𝑣 = 𝑑 β†’ (𝑐𝑑𝑣 ↔ 𝑐𝑑𝑑))
3029cbvrabv 3442 . . . . . . . 8 {𝑣 ∈ 𝐴 ∣ 𝑐𝑑𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}
3128, 30eqtrdi 2788 . . . . . . 7 (𝑒 = 𝑐 β†’ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣} = {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑})
3231cbvmptv 5261 . . . . . 6 (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ 𝑒𝑑𝑣}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑})
3326, 32eqtrdi 2788 . . . . 5 (π‘Ÿ = 𝑑 β†’ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}))
3433cbvmptv 5261 . . . 4 (π‘Ÿ ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑒 ∈ 𝐡 ↦ {𝑣 ∈ 𝐴 ∣ π‘’π‘Ÿπ‘£})) = (𝑑 ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}))
3523, 34eqtrdi 2788 . . 3 (πœ‘ β†’ (𝐡𝑅𝐴) = (𝑑 ∈ 𝒫 (𝐡 Γ— 𝐴) ↦ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑})))
36 breq 5150 . . . . . . 7 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐𝑑𝑑 ↔ 𝑐{βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}𝑑))
37 df-br 5149 . . . . . . . 8 (𝑐{βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}𝑑 ↔ βŸ¨π‘, π‘‘βŸ© ∈ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
38 vex 3478 . . . . . . . . 9 𝑐 ∈ V
39 vex 3478 . . . . . . . . 9 𝑑 ∈ V
40 eleq1w 2816 . . . . . . . . . 10 (𝑣 = 𝑐 β†’ (𝑣 ∈ (π‘“β€˜π‘’) ↔ 𝑐 ∈ (π‘“β€˜π‘’)))
4140anbi2d 629 . . . . . . . . 9 (𝑣 = 𝑐 β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ (𝑒 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘’))))
42 eleq1w 2816 . . . . . . . . . 10 (𝑒 = 𝑑 β†’ (𝑒 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
43 fveq2 6891 . . . . . . . . . . 11 (𝑒 = 𝑑 β†’ (π‘“β€˜π‘’) = (π‘“β€˜π‘‘))
4443eleq2d 2819 . . . . . . . . . 10 (𝑒 = 𝑑 β†’ (𝑐 ∈ (π‘“β€˜π‘’) ↔ 𝑐 ∈ (π‘“β€˜π‘‘)))
4542, 44anbi12d 631 . . . . . . . . 9 (𝑒 = 𝑑 β†’ ((𝑒 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘’)) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
4638, 39, 41, 45opelopab 5542 . . . . . . . 8 (βŸ¨π‘, π‘‘βŸ© ∈ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)))
4737, 46bitri 274 . . . . . . 7 (𝑐{βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)))
4836, 47bitrdi 286 . . . . . 6 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐𝑑𝑑 ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
4948rabbidv 3440 . . . . 5 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑} = {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))})
5049mpteq2dv 5250 . . . 4 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}) = (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}))
51 ibar 529 . . . . . . . . 9 (𝑑 ∈ 𝐴 β†’ (𝑐 ∈ (π‘“β€˜π‘‘) ↔ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))))
5251bicomd 222 . . . . . . . 8 (𝑑 ∈ 𝐴 β†’ ((𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘)) ↔ 𝑐 ∈ (π‘“β€˜π‘‘)))
5352rabbiia 3436 . . . . . . 7 {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))} = {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘‘)}
54 fveq2 6891 . . . . . . . . 9 (𝑑 = π‘₯ β†’ (π‘“β€˜π‘‘) = (π‘“β€˜π‘₯))
5554eleq2d 2819 . . . . . . . 8 (𝑑 = π‘₯ β†’ (𝑐 ∈ (π‘“β€˜π‘‘) ↔ 𝑐 ∈ (π‘“β€˜π‘₯)))
5655cbvrabv 3442 . . . . . . 7 {𝑑 ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘‘)} = {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}
5753, 56eqtri 2760 . . . . . 6 {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))} = {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}
5857mpteq2i 5253 . . . . 5 (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}) = (𝑐 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)})
59 eleq1w 2816 . . . . . . 7 (𝑐 = 𝑦 β†’ (𝑐 ∈ (π‘“β€˜π‘₯) ↔ 𝑦 ∈ (π‘“β€˜π‘₯)))
6059rabbidv 3440 . . . . . 6 (𝑐 = 𝑦 β†’ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)} = {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6160cbvmptv 5261 . . . . 5 (𝑐 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑐 ∈ (π‘“β€˜π‘₯)}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6258, 61eqtri 2760 . . . 4 (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ (𝑑 ∈ 𝐴 ∧ 𝑐 ∈ (π‘“β€˜π‘‘))}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})
6350, 62eqtrdi 2788 . . 3 (𝑑 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ (𝑐 ∈ 𝐡 ↦ {𝑑 ∈ 𝐴 ∣ 𝑐𝑑𝑑}) = (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)}))
6420, 21, 35, 63fmptco 7129 . 2 (πœ‘ β†’ ((𝐡𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
652, 1xpexd 7740 . . . . . 6 (πœ‘ β†’ (𝐴 Γ— 𝐡) ∈ V)
6665adantr 481 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (𝐴 Γ— 𝐡) ∈ V)
6712opabbidv 5214 . . . . . . 7 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
68 opabssxp 5768 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐡) ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡)
6967, 68eqsstrdi 4036 . . . . . 6 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡))
7069adantl 482 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} βŠ† (𝐴 Γ— 𝐡))
7166, 70sselpwd 5326 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} ∈ 𝒫 (𝐴 Γ— 𝐡))
72 eqid 2732 . . . . 5 (𝐴𝑅𝐡) = (𝐴𝑅𝐡)
7322, 2, 1, 72rfovcnvd 42838 . . . 4 (πœ‘ β†’ β—‘(𝐴𝑅𝐡) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
74 fsovd.cnv . . . . . 6 𝐢 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠))
7574a1i 11 . . . . 5 (πœ‘ β†’ 𝐢 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠)))
76 xpeq12 5701 . . . . . . . 8 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (π‘Ž Γ— 𝑏) = (𝐴 Γ— 𝐡))
7776pweqd 4619 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ 𝒫 (π‘Ž Γ— 𝑏) = 𝒫 (𝐴 Γ— 𝐡))
7877mpteq1d 5243 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
7978adantl 482 . . . . 5 ((πœ‘ ∧ (π‘Ž = 𝐴 ∧ 𝑏 = 𝐡)) β†’ (𝑠 ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ ◑𝑠) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
802elexd 3494 . . . . 5 (πœ‘ β†’ 𝐴 ∈ V)
811elexd 3494 . . . . 5 (πœ‘ β†’ 𝐡 ∈ V)
82 pwexg 5376 . . . . . 6 ((𝐴 Γ— 𝐡) ∈ V β†’ 𝒫 (𝐴 Γ— 𝐡) ∈ V)
83 mptexg 7225 . . . . . 6 (𝒫 (𝐴 Γ— 𝐡) ∈ V β†’ (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠) ∈ V)
8465, 82, 833syl 18 . . . . 5 (πœ‘ β†’ (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠) ∈ V)
8575, 79, 80, 81, 84ovmpod 7562 . . . 4 (πœ‘ β†’ (𝐴𝐢𝐡) = (𝑠 ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ ◑𝑠))
86 cnveq 5873 . . . . 5 (𝑠 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ ◑𝑠 = β—‘{βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
87 cnvopab 6138 . . . . 5 β—‘{βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}
8886, 87eqtrdi 2788 . . . 4 (𝑠 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))} β†’ ◑𝑠 = {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})
8971, 73, 85, 88fmptco 7129 . . 3 (πœ‘ β†’ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡)) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))}))
9089coeq2d 5862 . 2 (πœ‘ β†’ ((𝐡𝑅𝐴) ∘ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡))) = ((𝐡𝑅𝐴) ∘ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {βŸ¨π‘£, π‘’βŸ© ∣ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))})))
91 fsovd.fs . . 3 𝑂 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m π‘Ž) ↦ (𝑦 ∈ 𝑏 ↦ {π‘₯ ∈ π‘Ž ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
9291, 2, 1fsovd 42841 . 2 (πœ‘ β†’ (𝐴𝑂𝐡) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ (𝑦 ∈ 𝐡 ↦ {π‘₯ ∈ 𝐴 ∣ 𝑦 ∈ (π‘“β€˜π‘₯)})))
9364, 90, 923eqtr4rd 2783 1 (πœ‘ β†’ (𝐴𝑂𝐡) = ((𝐡𝑅𝐴) ∘ ((𝐴𝐢𝐡) ∘ β—‘(𝐴𝑅𝐡))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3432  Vcvv 3474   βŠ† wss 3948  π’« cpw 4602  βŸ¨cop 4634   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675   ∘ ccom 5680  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413   ↑m cmap 8822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-map 8824
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator