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