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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑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 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑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 eqtrid ⊢ ( 𝑥 = 𝑎 → { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } = { 𝑏 ∈ 𝐵 ∣ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑟 } )
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 eqtrid ⊢ ( 𝜑 → 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
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 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ) )