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