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 
|- A e. _V
fpwrelmap.2 
|- B e. _V
fpwrelmap.3 
|- M = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
Assertion fpwrelmap 
|- M : ( ~P B ^m A ) -1-1-onto-> ~P ( A X. B )

Proof

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