Metamath Proof Explorer


Theorem rfovcnvf1od

Description: Properties of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses rfovd.rf 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥𝑎 ↦ { 𝑦𝑏𝑥 𝑟 𝑦 } ) ) )
rfovd.a ( 𝜑𝐴𝑉 )
rfovd.b ( 𝜑𝐵𝑊 )
rfovcnvf1od.f 𝐹 = ( 𝐴 𝑂 𝐵 )
Assertion rfovcnvf1od ( 𝜑 → ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 rfovd.rf 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥𝑎 ↦ { 𝑦𝑏𝑥 𝑟 𝑦 } ) ) )
2 rfovd.a ( 𝜑𝐴𝑉 )
3 rfovd.b ( 𝜑𝐵𝑊 )
4 rfovcnvf1od.f 𝐹 = ( 𝐴 𝑂 𝐵 )
5 eqid ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) )
6 ssrab2 { 𝑦𝐵𝑥 𝑟 𝑦 } ⊆ 𝐵
7 6 a1i ( 𝜑 → { 𝑦𝐵𝑥 𝑟 𝑦 } ⊆ 𝐵 )
8 3 7 sselpwd ( 𝜑 → { 𝑦𝐵𝑥 𝑟 𝑦 } ∈ 𝒫 𝐵 )
9 8 adantr ( ( 𝜑𝑥𝐴 ) → { 𝑦𝐵𝑥 𝑟 𝑦 } ∈ 𝒫 𝐵 )
10 9 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) : 𝐴 ⟶ 𝒫 𝐵 )
11 3 pwexd ( 𝜑 → 𝒫 𝐵 ∈ V )
12 11 2 elmapd ( 𝜑 → ( ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ∈ ( 𝒫 𝐵m 𝐴 ) ↔ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) : 𝐴 ⟶ 𝒫 𝐵 ) )
13 10 12 mpbird ( 𝜑 → ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ∈ ( 𝒫 𝐵m 𝐴 ) )
14 13 adantr ( ( 𝜑𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) → ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ∈ ( 𝒫 𝐵m 𝐴 ) )
15 2 3 xpexd ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
16 15 adantr ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → ( 𝐴 × 𝐵 ) ∈ V )
17 11 2 elmapd ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝒫 𝐵 ) )
18 17 biimpa ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
19 18 ffvelrnda ( ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ∧ 𝑥𝐴 ) → ( 𝑓𝑥 ) ∈ 𝒫 𝐵 )
20 19 ex ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → ( 𝑥𝐴 → ( 𝑓𝑥 ) ∈ 𝒫 𝐵 ) )
21 elpwi ( ( 𝑓𝑥 ) ∈ 𝒫 𝐵 → ( 𝑓𝑥 ) ⊆ 𝐵 )
22 21 sseld ( ( 𝑓𝑥 ) ∈ 𝒫 𝐵 → ( 𝑦 ∈ ( 𝑓𝑥 ) → 𝑦𝐵 ) )
23 20 22 syl6 ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → ( 𝑥𝐴 → ( 𝑦 ∈ ( 𝑓𝑥 ) → 𝑦𝐵 ) ) )
24 23 imdistand ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → ( ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) → ( 𝑥𝐴𝑦𝐵 ) ) )
25 trud ( ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) → ⊤ )
26 24 25 jca2 ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → ( ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) → ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⊤ ) ) )
27 26 ssopab2dv ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⊤ ) } )
28 opabssxp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⊤ ) } ⊆ ( 𝐴 × 𝐵 )
29 27 28 sstrdi ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ⊆ ( 𝐴 × 𝐵 ) )
30 16 29 sselpwd ( ( 𝜑𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ∈ 𝒫 ( 𝐴 × 𝐵 ) )
31 simplrr ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) → 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) )
32 elmapfn ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) → 𝑓 Fn 𝐴 )
33 31 32 syl ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) → 𝑓 Fn 𝐴 )
34 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) → 𝐵𝑊 )
35 rabexg ( 𝐵𝑊 → { 𝑦𝐵𝑥 𝑟 𝑦 } ∈ V )
36 35 ralrimivw ( 𝐵𝑊 → ∀ 𝑥𝐴 { 𝑦𝐵𝑥 𝑟 𝑦 } ∈ V )
37 nfcv 𝑥 𝐴
38 37 fnmptf ( ∀ 𝑥𝐴 { 𝑦𝐵𝑥 𝑟 𝑦 } ∈ V → ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) Fn 𝐴 )
39 34 36 38 3syl ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) → ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) Fn 𝐴 )
40 dfin5 ( 𝐵 ∩ ( 𝑓𝑢 ) ) = { 𝑏𝐵𝑏 ∈ ( 𝑓𝑢 ) }
41 simpllr ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) )
42 elmapi ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
43 41 42 simpl2im ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
44 simpr ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → 𝑢𝐴 )
45 43 44 ffvelrnd ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝑓𝑢 ) ∈ 𝒫 𝐵 )
46 45 elpwid ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝑓𝑢 ) ⊆ 𝐵 )
47 sseqin2 ( ( 𝑓𝑢 ) ⊆ 𝐵 ↔ ( 𝐵 ∩ ( 𝑓𝑢 ) ) = ( 𝑓𝑢 ) )
48 46 47 sylib ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝐵 ∩ ( 𝑓𝑢 ) ) = ( 𝑓𝑢 ) )
49 ibar ( 𝑢𝐴 → ( 𝑏 ∈ ( 𝑓𝑢 ) ↔ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) ) )
50 49 rabbidv ( 𝑢𝐴 → { 𝑏𝐵𝑏 ∈ ( 𝑓𝑢 ) } = { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } )
51 50 adantl ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → { 𝑏𝐵𝑏 ∈ ( 𝑓𝑢 ) } = { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } )
52 40 48 51 3eqtr3a ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝑓𝑢 ) = { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } )
53 breq2 ( 𝑦 = 𝑏 → ( 𝑥 𝑟 𝑦𝑥 𝑟 𝑏 ) )
54 53 cbvrabv { 𝑦𝐵𝑥 𝑟 𝑦 } = { 𝑏𝐵𝑥 𝑟 𝑏 }
55 breq1 ( 𝑥 = 𝑎 → ( 𝑥 𝑟 𝑏𝑎 𝑟 𝑏 ) )
56 df-br ( 𝑎 𝑟 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 )
57 55 56 bitrdi ( 𝑥 = 𝑎 → ( 𝑥 𝑟 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 ) )
58 57 rabbidv ( 𝑥 = 𝑎 → { 𝑏𝐵𝑥 𝑟 𝑏 } = { 𝑏𝐵 ∣ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 } )
59 54 58 syl5eq ( 𝑥 = 𝑎 → { 𝑦𝐵𝑥 𝑟 𝑦 } = { 𝑏𝐵 ∣ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 } )
60 59 cbvmptv ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) = ( 𝑎𝐴 ↦ { 𝑏𝐵 ∣ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 } )
61 simpr ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → 𝑎 = 𝑢 )
62 61 opeq1d ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑏 ⟩ )
63 simpllr ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } )
64 62 63 eleq12d ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 ↔ ⟨ 𝑢 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) )
65 vex 𝑢 ∈ V
66 vex 𝑏 ∈ V
67 simpl ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → 𝑥 = 𝑢 )
68 67 eleq1d ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → ( 𝑥𝐴𝑢𝐴 ) )
69 simpr ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → 𝑦 = 𝑏 )
70 67 fveq2d ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → ( 𝑓𝑥 ) = ( 𝑓𝑢 ) )
71 69 70 eleq12d ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → ( 𝑦 ∈ ( 𝑓𝑥 ) ↔ 𝑏 ∈ ( 𝑓𝑢 ) ) )
72 68 71 anbi12d ( ( 𝑥 = 𝑢𝑦 = 𝑏 ) → ( ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) ↔ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) ) )
73 65 66 72 opelopaba ( ⟨ 𝑢 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ↔ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) )
74 64 73 bitrdi ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 ↔ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) ) )
75 74 rabbidv ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → { 𝑏𝐵 ∣ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 } = { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } )
76 3 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → 𝐵𝑊 )
77 rabexg ( 𝐵𝑊 → { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } ∈ V )
78 76 77 syl ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } ∈ V )
79 60 75 44 78 fvmptd2 ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ‘ 𝑢 ) = { 𝑏𝐵 ∣ ( 𝑢𝐴𝑏 ∈ ( 𝑓𝑢 ) ) } )
80 52 79 eqtr4d ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ 𝑢𝐴 ) → ( 𝑓𝑢 ) = ( ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ‘ 𝑢 ) )
81 33 39 80 eqfnfvd ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) → 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) )
82 simplrl ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
83 82 elpwid ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
84 xpss ( 𝐴 × 𝐵 ) ⊆ ( V × V )
85 83 84 sstrdi ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 ⊆ ( V × V ) )
86 df-rel ( Rel 𝑟𝑟 ⊆ ( V × V ) )
87 85 86 sylibr ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → Rel 𝑟 )
88 relopabv Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) }
89 88 a1i ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } )
90 simpl ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
91 3 90 anim12i ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) → ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) )
92 91 anim1i ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) )
93 vex 𝑣 ∈ V
94 simpl ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
95 94 eleq1d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( 𝑥𝐴𝑢𝐴 ) )
96 simpr ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
97 94 fveq2d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( 𝑓𝑥 ) = ( 𝑓𝑢 ) )
98 96 97 eleq12d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( 𝑦 ∈ ( 𝑓𝑥 ) ↔ 𝑣 ∈ ( 𝑓𝑢 ) ) )
99 95 98 anbi12d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) ↔ ( 𝑢𝐴𝑣 ∈ ( 𝑓𝑢 ) ) ) )
100 65 93 99 opelopaba ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ↔ ( 𝑢𝐴𝑣 ∈ ( 𝑓𝑢 ) ) )
101 breq2 ( 𝑏 = 𝑣 → ( 𝑢 𝑟 𝑏𝑢 𝑟 𝑣 ) )
102 df-br ( 𝑢 𝑟 𝑣 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 )
103 101 102 bitrdi ( 𝑏 = 𝑣 → ( 𝑢 𝑟 𝑏 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) )
104 103 elrab ( 𝑣 ∈ { 𝑏𝐵𝑢 𝑟 𝑏 } ↔ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) )
105 104 anbi2i ( ( 𝑢𝐴𝑣 ∈ { 𝑏𝐵𝑢 𝑟 𝑏 } ) ↔ ( 𝑢𝐴 ∧ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) )
106 105 a1i ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ( 𝑢𝐴𝑣 ∈ { 𝑏𝐵𝑢 𝑟 𝑏 } ) ↔ ( 𝑢𝐴 ∧ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) ) )
107 simplr ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) )
108 breq1 ( 𝑥 = 𝑎 → ( 𝑥 𝑟 𝑦𝑎 𝑟 𝑦 ) )
109 108 rabbidv ( 𝑥 = 𝑎 → { 𝑦𝐵𝑥 𝑟 𝑦 } = { 𝑦𝐵𝑎 𝑟 𝑦 } )
110 breq2 ( 𝑦 = 𝑏 → ( 𝑎 𝑟 𝑦𝑎 𝑟 𝑏 ) )
111 110 cbvrabv { 𝑦𝐵𝑎 𝑟 𝑦 } = { 𝑏𝐵𝑎 𝑟 𝑏 }
112 109 111 eqtrdi ( 𝑥 = 𝑎 → { 𝑦𝐵𝑥 𝑟 𝑦 } = { 𝑏𝐵𝑎 𝑟 𝑏 } )
113 112 cbvmptv ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) = ( 𝑎𝐴 ↦ { 𝑏𝐵𝑎 𝑟 𝑏 } )
114 107 113 eqtrdi ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → 𝑓 = ( 𝑎𝐴 ↦ { 𝑏𝐵𝑎 𝑟 𝑏 } ) )
115 breq1 ( 𝑎 = 𝑢 → ( 𝑎 𝑟 𝑏𝑢 𝑟 𝑏 ) )
116 115 rabbidv ( 𝑎 = 𝑢 → { 𝑏𝐵𝑎 𝑟 𝑏 } = { 𝑏𝐵𝑢 𝑟 𝑏 } )
117 116 adantl ( ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) ∧ 𝑎 = 𝑢 ) → { 𝑏𝐵𝑎 𝑟 𝑏 } = { 𝑏𝐵𝑢 𝑟 𝑏 } )
118 simpr ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → 𝑢𝐴 )
119 rabexg ( 𝐵𝑊 → { 𝑏𝐵𝑢 𝑟 𝑏 } ∈ V )
120 119 ad3antrrr ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → { 𝑏𝐵𝑢 𝑟 𝑏 } ∈ V )
121 114 117 118 120 fvmptd ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → ( 𝑓𝑢 ) = { 𝑏𝐵𝑢 𝑟 𝑏 } )
122 121 eleq2d ( ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ∧ 𝑢𝐴 ) → ( 𝑣 ∈ ( 𝑓𝑢 ) ↔ 𝑣 ∈ { 𝑏𝐵𝑢 𝑟 𝑏 } ) )
123 122 pm5.32da ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ( 𝑢𝐴𝑣 ∈ ( 𝑓𝑢 ) ) ↔ ( 𝑢𝐴𝑣 ∈ { 𝑏𝐵𝑢 𝑟 𝑏 } ) ) )
124 simplr ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
125 124 elpwid ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
126 65 93 opeldm ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟𝑢 ∈ dom 𝑟 )
127 dmss ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑟 ⊆ dom ( 𝐴 × 𝐵 ) )
128 dmxpss dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
129 127 128 sstrdi ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑟𝐴 )
130 129 sseld ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑢 ∈ dom 𝑟𝑢𝐴 ) )
131 126 130 syl5 ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟𝑢𝐴 ) )
132 131 pm4.71rd ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ↔ ( 𝑢𝐴 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) )
133 65 93 opelrn ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟𝑣 ∈ ran 𝑟 )
134 rnss ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑟 ⊆ ran ( 𝐴 × 𝐵 ) )
135 rnxpss ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
136 134 135 sstrdi ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑟𝐵 )
137 136 sseld ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑣 ∈ ran 𝑟𝑣𝐵 ) )
138 133 137 syl5 ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟𝑣𝐵 ) )
139 138 pm4.71rd ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ↔ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) )
140 139 anbi2d ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ( 𝑢𝐴 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ↔ ( 𝑢𝐴 ∧ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) ) )
141 132 140 bitrd ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ↔ ( 𝑢𝐴 ∧ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) ) )
142 125 141 syl ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ↔ ( 𝑢𝐴 ∧ ( 𝑣𝐵 ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) ) ) )
143 106 123 142 3bitr4d ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ( 𝑢𝐴𝑣 ∈ ( 𝑓𝑢 ) ) ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ) )
144 100 143 bitr2id ( ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑟 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) )
145 144 eqrelrdv2 ( ( ( Rel 𝑟 ∧ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ∧ ( ( 𝐵𝑊𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } )
146 87 89 92 145 syl21anc ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) ∧ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } )
147 81 146 impbida ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ) ) → ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ↔ 𝑓 = ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) )
148 5 14 30 147 f1ocnv2d ( 𝜑 → ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) )
149 1 2 3 rfovd ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) )
150 4 149 syl5eq ( 𝜑𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) )
151 f1oeq1 ( 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ↔ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ) )
152 cnveq ( 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) )
153 152 eqeq1d ( 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ↔ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) )
154 151 153 anbi12d ( 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) → ( ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) ↔ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) ) )
155 150 154 syl ( 𝜑 → ( ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) ↔ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥𝐴 ↦ { 𝑦𝐵𝑥 𝑟 𝑦 } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) ) )
156 148 155 mpbird ( 𝜑 → ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝐴 ) ∧ 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) ) )