Metamath Proof Explorer

Theorem fsovrfovd

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)

Ref Expression
Hypotheses fsovd.fs ⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
fsovd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fsovd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
fsovd.rf ⊢ 𝑅 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑢 ∈ 𝑎 ↦ { 𝑣 ∈ 𝑏 ∣ 𝑢 𝑟 𝑣 } ) ) )
fsovd.cnv ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ◡ 𝑠 ) )
Assertion fsovrfovd ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( ( 𝐵 𝑅 𝐴 ) ∘ ( ( 𝐴 𝐶 𝐵 ) ∘ ◡ ( 𝐴 𝑅 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 fsovd.fs ⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
2 fsovd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fsovd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 fsovd.rf ⊢ 𝑅 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑢 ∈ 𝑎 ↦ { 𝑣 ∈ 𝑏 ∣ 𝑢 𝑟 𝑣 } ) ) )
5 fsovd.cnv ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ◡ 𝑠 ) )
6 3 2 xpexd ⊢ ( 𝜑 → ( 𝐵 × 𝐴 ) ∈ V )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝐵 × 𝐴 ) ∈ V )
8 elmapi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
9 8 ffvelcdmda ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ∈ 𝒫 𝐵 )
10 9 elpwid ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑢 ) ⊆ 𝐵 )
11 10 sseld ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) → 𝑣 ∈ 𝐵 ) )
12 11 impancom ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑢 ∈ 𝐴 → 𝑣 ∈ 𝐵 ) )
13 12 pm4.71d ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑢 ∈ 𝐴 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) )
14 13 ex ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) → ( 𝑢 ∈ 𝐴 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ) )
15 14 pm5.32rd ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
16 ancom ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ↔ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) )
17 16 anbi1i ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ↔ ( ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) )
18 15 17 bitrdi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ↔ ( ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
19 18 opabbidv ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } )
20 opabssxp ⊢ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐵 × 𝐴 )
21 19 20 eqsstrdi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐵 × 𝐴 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐵 × 𝐴 ) )
23 7 22 sselpwd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ∈ 𝒫 ( 𝐵 × 𝐴 ) )
24 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) )
25 4 3 2 rfovd ⊢ ( 𝜑 → ( 𝐵 𝑅 𝐴 ) = ( 𝑟 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↦ ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑟 𝑣 } ) ) )
26 breq ⊢ ( 𝑟 = 𝑡 → ( 𝑢 𝑟 𝑣 ↔ 𝑢 𝑡 𝑣 ) )
27 26 rabbidv ⊢ ( 𝑟 = 𝑡 → { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑟 𝑣 } = { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑡 𝑣 } )
28 27 mpteq2dv ⊢ ( 𝑟 = 𝑡 → ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑟 𝑣 } ) = ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑡 𝑣 } ) )
29 breq1 ⊢ ( 𝑢 = 𝑐 → ( 𝑢 𝑡 𝑣 ↔ 𝑐 𝑡 𝑣 ) )
30 29 rabbidv ⊢ ( 𝑢 = 𝑐 → { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑡 𝑣 } = { 𝑣 ∈ 𝐴 ∣ 𝑐 𝑡 𝑣 } )
31 breq2 ⊢ ( 𝑣 = 𝑑 → ( 𝑐 𝑡 𝑣 ↔ 𝑐 𝑡 𝑑 ) )
32 31 cbvrabv ⊢ { 𝑣 ∈ 𝐴 ∣ 𝑐 𝑡 𝑣 } = { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 }
33 30 32 eqtrdi ⊢ ( 𝑢 = 𝑐 → { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑡 𝑣 } = { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } )
34 33 cbvmptv ⊢ ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑡 𝑣 } ) = ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } )
35 28 34 eqtrdi ⊢ ( 𝑟 = 𝑡 → ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑟 𝑣 } ) = ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } ) )
36 35 cbvmptv ⊢ ( 𝑟 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↦ ( 𝑢 ∈ 𝐵 ↦ { 𝑣 ∈ 𝐴 ∣ 𝑢 𝑟 𝑣 } ) ) = ( 𝑡 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↦ ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } ) )
37 25 36 eqtrdi ⊢ ( 𝜑 → ( 𝐵 𝑅 𝐴 ) = ( 𝑡 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↦ ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } ) ) )
38 breq ⊢ ( 𝑡 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ( 𝑐 𝑡 𝑑 ↔ 𝑐 { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } 𝑑 ) )
39 df-br ⊢ ( 𝑐 { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } 𝑑 ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } )
40 vex ⊢ 𝑐 ∈ V
41 vex ⊢ 𝑑 ∈ V
42 eleq1w ⊢ ( 𝑣 = 𝑐 → ( 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ↔ 𝑐 ∈ ( 𝑓 ‘ 𝑢 ) ) )
43 42 anbi2d ⊢ ( 𝑣 = 𝑐 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
44 eleq1w ⊢ ( 𝑢 = 𝑑 → ( 𝑢 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴 ) )
45 fveq2 ⊢ ( 𝑢 = 𝑑 → ( 𝑓 ‘ 𝑢 ) = ( 𝑓 ‘ 𝑑 ) )
46 45 eleq2d ⊢ ( 𝑢 = 𝑑 → ( 𝑐 ∈ ( 𝑓 ‘ 𝑢 ) ↔ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) )
47 44 46 anbi12d ⊢ ( 𝑢 = 𝑑 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑢 ) ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) ) )
48 40 41 43 47 opelopab ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) )
49 39 48 bitri ⊢ ( 𝑐 { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } 𝑑 ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) )
50 38 49 bitrdi ⊢ ( 𝑡 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ( 𝑐 𝑡 𝑑 ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) ) )
51 50 rabbidv ⊢ ( 𝑡 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } = { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } )
52 51 mpteq2dv ⊢ ( 𝑡 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } ) = ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } ) )
53 ibar ⊢ ( 𝑑 ∈ 𝐴 → ( 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) ) )
54 53 bicomd ⊢ ( 𝑑 ∈ 𝐴 → ( ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) ↔ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) )
55 54 rabbiia ⊢ { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } = { 𝑑 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) }
56 fveq2 ⊢ ( 𝑑 = 𝑥 → ( 𝑓 ‘ 𝑑 ) = ( 𝑓 ‘ 𝑥 ) )
57 56 eleq2d ⊢ ( 𝑑 = 𝑥 → ( 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ↔ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) ) )
58 57 cbvrabv ⊢ { 𝑑 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) }
59 55 58 eqtri ⊢ { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } = { 𝑥 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) }
60 59 mpteq2i ⊢ ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } ) = ( 𝑐 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) } )
61 eleq1w ⊢ ( 𝑐 = 𝑦 → ( 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
62 61 rabbidv ⊢ ( 𝑐 = 𝑦 → { 𝑥 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } )
63 62 cbvmptv ⊢ ( 𝑐 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑐 ∈ ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } )
64 60 63 eqtri ⊢ ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ ( 𝑓 ‘ 𝑑 ) ) } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } )
65 52 64 eqtrdi ⊢ ( 𝑡 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ( 𝑐 ∈ 𝐵 ↦ { 𝑑 ∈ 𝐴 ∣ 𝑐 𝑡 𝑑 } ) = ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) )
66 23 24 37 65 fmptco ⊢ ( 𝜑 → ( ( 𝐵 𝑅 𝐴 ) ∘ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
67 2 3 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → ( 𝐴 × 𝐵 ) ∈ V )
69 15 opabbidv ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } )
70 opabssxp ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐴 × 𝐵 )
71 69 70 eqsstrdi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐴 × 𝐵 ) )
72 71 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ⊆ ( 𝐴 × 𝐵 ) )
73 68 72 sselpwd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ∈ 𝒫 ( 𝐴 × 𝐵 ) )
74 eqid ⊢ ( 𝐴 𝑅 𝐵 ) = ( 𝐴 𝑅 𝐵 )
75 4 2 3 74 rfovcnvd ⊢ ( 𝜑 → ◡ ( 𝐴 𝑅 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) )
76 5 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ◡ 𝑠 ) ) )
77 xpeq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 × 𝑏 ) = ( 𝐴 × 𝐵 ) )
78 77 pweqd ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( 𝐴 × 𝐵 ) )
79 78 mpteq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑠 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ◡ 𝑠 ) = ( 𝑠 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ◡ 𝑠 ) )
80 79 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑠 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ◡ 𝑠 ) = ( 𝑠 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ◡ 𝑠 ) )
81 2 elexd ⊢ ( 𝜑 → 𝐴 ∈ V )
82 3 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
83 pwexg ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
84 mptexg ⊢ ( 𝒫 ( 𝐴 × 𝐵 ) ∈ V → ( 𝑠 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ◡ 𝑠 ) ∈ V )
85 67 83 84 3syl ⊢ ( 𝜑 → ( 𝑠 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ◡ 𝑠 ) ∈ V )
86 76 80 81 82 85 ovmpod ⊢ ( 𝜑 → ( 𝐴 𝐶 𝐵 ) = ( 𝑠 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ◡ 𝑠 ) )
87 cnveq ⊢ ( 𝑠 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ◡ 𝑠 = ◡ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } )
88 cnvopab ⊢ ◡ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) }
89 87 88 eqtrdi ⊢ ( 𝑠 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } → ◡ 𝑠 = { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } )
90 73 75 86 89 fmptco ⊢ ( 𝜑 → ( ( 𝐴 𝐶 𝐵 ) ∘ ◡ ( 𝐴 𝑅 𝐵 ) ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) )
91 90 coeq2d ⊢ ( 𝜑 → ( ( 𝐵 𝑅 𝐴 ) ∘ ( ( 𝐴 𝐶 𝐵 ) ∘ ◡ ( 𝐴 𝑅 𝐵 ) ) ) = ( ( 𝐵 𝑅 𝐴 ) ∘ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑣 , 𝑢 ⟩ ∣ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝑓 ‘ 𝑢 ) ) } ) ) )
92 1 2 3 fsovd ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
93 66 91 92 3eqtr4rd ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( ( 𝐵 𝑅 𝐴 ) ∘ ( ( 𝐴 𝐶 𝐵 ) ∘ ◡ ( 𝐴 𝑅 𝐵 ) ) ) )