This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpwrelmap

Description: Define a canonical mapping between functions from A into subsets of B and the relations with domain A and range within B . Note that the same relation is used in axdc2lem and marypha2lem1 . (Contributed by Thierry Arnoux, 28-Aug-2017)

Ref Expression
Hypotheses fpwrelmap.1 ⊢ 𝐴 ∈ V
fpwrelmap.2 ⊢ 𝐵 ∈ V
fpwrelmap.3 ⊢ 𝑀 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
Assertion fpwrelmap 𝑀 : ( 𝒫 𝐵 ↑m 𝐴 ) –1-1-onto→ 𝒫 ( 𝐴 × 𝐵 )

Proof

Step Hyp Ref Expression
1 fpwrelmap.1 ⊢ 𝐴 ∈ V
2 fpwrelmap.2 ⊢ 𝐵 ∈ V
3 fpwrelmap.3 ⊢ 𝑀 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
4 1 a1i ⊢ ( ⊤ → 𝐴 ∈ V )
5 abid2 ⊢ { 𝑦 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = ( 𝑓 ‘ 𝑥 )
6 5 fvexi ⊢ { 𝑦 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ V
7 6 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ∈ V )
8 4 7 opabex3d ⊢ ( ⊤ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ∈ V )
9 8 adantr ⊢ ( ( ⊤ ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ∈ V )
10 1 mptex ⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ∈ V
11 10 a1i ⊢ ( ( ⊤ ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ∈ V )
12 simpr ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) )
13 elmapi ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
14 13 ffvelcdmda ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝒫 𝐵 )
15 14 adantr ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝒫 𝐵 )
16 elelpwi ⊢ ( ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝒫 𝐵 ) → 𝑦 ∈ 𝐵 )
17 12 15 16 syl2anc ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐵 )
18 17 ex ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) → 𝑦 ∈ 𝐵 ) )
19 18 imdistanda ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
20 19 ssopab2dv ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } )
21 20 adantr ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } )
22 simpr ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
23 df-xp ⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
24 23 a1i ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } )
25 21 22 24 3sstr4d ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
26 velpw ⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
27 25 26 sylibr ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
28 13 feqmptd ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑥 ) ) )
29 28 adantr ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑓 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑥 ) ) )
30 nfv ⊢ Ⅎ 𝑥 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 )
31 nfopab1 ⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) }
32 31 nfeq2 ⊢ Ⅎ 𝑥 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) }
33 30 32 nfan ⊢ Ⅎ 𝑥 ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
34 df-rab ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) }
35 34 a1i ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) } )
36 nfv ⊢ Ⅎ 𝑦 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 )
37 nfopab2 ⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) }
38 37 nfeq2 ⊢ Ⅎ 𝑦 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) }
39 36 38 nfan ⊢ Ⅎ 𝑦 ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
40 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
41 39 40 nfan ⊢ Ⅎ 𝑦 ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 )
42 17 adantllr ⊢ ( ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐵 )
43 df-br ⊢ ( 𝑥 𝑟 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 )
44 eleq2 ⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) )
45 opabidw ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
46 44 45 bitrdi ⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
47 43 46 bitrid ⊢ ( 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } → ( 𝑥 𝑟 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
48 47 ad2antlr ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑟 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
49 elfvdm ⊢ ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) → 𝑥 ∈ dom 𝑓 )
50 49 adantl ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑥 ∈ dom 𝑓 )
51 13 fdmd ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → dom 𝑓 = 𝐴 )
52 51 adantr ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → dom 𝑓 = 𝐴 )
53 50 52 eleqtrd ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
54 53 ex ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) → 𝑥 ∈ 𝐴 ) )
55 54 pm4.71rd ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
56 55 ad2antrr ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
57 48 56 bitr4d ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑟 𝑦 ↔ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
58 57 biimpar ⊢ ( ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑥 𝑟 𝑦 )
59 42 58 jca ⊢ ( ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) )
60 59 ex ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) ) )
61 57 biimpd ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑟 𝑦 → 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
62 61 adantld ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) → 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
63 60 62 impbid ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) ) )
64 41 63 abbid ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) } )
65 5 a1i ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } = ( 𝑓 ‘ 𝑥 ) )
66 35 64 65 3eqtr2rd ⊢ ( ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
67 33 66 mpteq2da ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
68 29 67 eqtrd ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
69 27 68 jca ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
70 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ⊆ 𝐵
71 2 70 elpwi2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ∈ 𝒫 𝐵
72 71 a1i ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ∈ 𝒫 𝐵 )
73 72 fmpttd ⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) : 𝐴 ⟶ 𝒫 𝐵 )
74 73 adantr ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) : 𝐴 ⟶ 𝒫 𝐵 )
75 simpr ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
76 75 feq1d ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑓 : 𝐴 ⟶ 𝒫 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) : 𝐴 ⟶ 𝒫 𝐵 ) )
77 74 76 mpbird ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
78 2 pwex ⊢ 𝒫 𝐵 ∈ V
79 78 1 elmap ⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝒫 𝐵 )
80 77 79 sylibr ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) )
81 elpwi ⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) → 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
82 81 adantr ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑟 ⊆ ( 𝐴 × 𝐵 ) )
83 xpss ⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
84 82 83 sstrdi ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑟 ⊆ ( V × V ) )
85 df-rel ⊢ ( Rel 𝑟 ↔ 𝑟 ⊆ ( V × V ) )
86 84 85 sylibr ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → Rel 𝑟 )
87 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) }
88 87 a1i ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
89 id ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
90 nfv ⊢ Ⅎ 𝑥 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 )
91 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
92 91 nfeq2 ⊢ Ⅎ 𝑥 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
93 90 92 nfan ⊢ Ⅎ 𝑥 ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
94 nfv ⊢ Ⅎ 𝑦 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 )
95 40 nfci ⊢ Ⅎ 𝑦 𝐴
96 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 }
97 95 96 nfmpt ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
98 97 nfeq2 ⊢ Ⅎ 𝑦 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
99 94 98 nfan ⊢ Ⅎ 𝑦 ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
100 nfcv ⊢ Ⅎ 𝑥 𝑟
101 nfcv ⊢ Ⅎ 𝑦 𝑟
102 brelg ⊢ ( ( 𝑟 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑥 𝑟 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
103 81 102 sylan ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑥 𝑟 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
104 103 adantlr ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
105 104 simpld ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → 𝑥 ∈ 𝐴 )
106 104 simprd ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → 𝑦 ∈ 𝐵 )
107 simpr ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → 𝑥 𝑟 𝑦 )
108 75 fveq1d ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ‘ 𝑥 ) )
109 2 rabex ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ∈ V
110 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
111 110 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ‘ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
112 109 111 mpan2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ‘ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
113 108 112 sylan9eq ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
114 113 eleq2d ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
115 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) )
116 114 115 bitrdi ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) ) )
117 105 116 syldan ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → ( 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝑟 𝑦 ) ) )
118 106 107 117 mpbir2and ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) )
119 105 118 jca ⊢ ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 𝑟 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) )
120 119 ex ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑥 𝑟 𝑦 → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
121 116 simplbda ⊢ ( ( ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑥 𝑟 𝑦 )
122 121 expl ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝑥 𝑟 𝑦 ) )
123 120 122 impbid ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑥 𝑟 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
124 43 123 bitr3id ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
125 124 45 bitr4di ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) )
126 93 99 100 101 31 37 125 eqrelrd2 ⊢ ( ( ( Rel 𝑟 ∧ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ∧ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
127 86 88 89 126 syl21anc ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } )
128 80 127 jca ⊢ ( ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) )
129 69 128 impbii ⊢ ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ↔ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
130 129 a1i ⊢ ( ⊤ → ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ 𝑟 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ↔ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ) )
131 3 9 11 130 f1od ⊢ ( ⊤ → 𝑀 : ( 𝒫 𝐵 ↑m 𝐴 ) –1-1-onto→ 𝒫 ( 𝐴 × 𝐵 ) )
132 131 mptru ⊢ 𝑀 : ( 𝒫 𝐵 ↑m 𝐴 ) –1-1-onto→ 𝒫 ( 𝐴 × 𝐵 )