Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fpwrelmap Structured version   Visualization version   Unicode version

Theorem fpwrelmap 28393
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 8896 and marypha2lem1 7967. (Contributed by Thierry Arnoux, 28-Aug-2017.)
Hypotheses
Ref Expression
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
Ref Expression
fpwrelmap  |-  M :
( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B )
Distinct variable groups:    x, f,
y, A    B, f, x, y
Allowed substitution hints:    M( x, y, f)

Proof of Theorem fpwrelmap
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 fpwrelmap.3 . . 3  |-  M  =  ( f  e.  ( ~P B  ^m  A
)  |->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) } )
2 fpwrelmap.1 . . . . . 6  |-  A  e. 
_V
32a1i 11 . . . . 5  |-  ( f  e.  ( ~P B  ^m  A )  ->  A  e.  _V )
4 simpr 468 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  ( f `  x
) )
5 elmapi 7511 . . . . . . . . . . 11  |-  ( f  e.  ( ~P B  ^m  A )  ->  f : A --> ~P B )
65ffvelrnda 6037 . . . . . . . . . 10  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( f `  x )  e.  ~P B )
76adantr 472 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  (
f `  x )  e.  ~P B )
8 elelpwi 3953 . . . . . . . . 9  |-  ( ( y  e.  ( f `
 x )  /\  ( f `  x
)  e.  ~P B
)  ->  y  e.  B )
94, 7, 8syl2anc 673 . . . . . . . 8  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  B )
109ex 441 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( y  e.  ( f `  x
)  ->  y  e.  B ) )
1110alrimiv 1781 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  A. y
( y  e.  ( f `  x )  ->  y  e.  B
) )
12 abss 3484 . . . . . . 7  |-  ( { y  |  y  e.  ( f `  x
) }  C_  B  <->  A. y ( y  e.  ( f `  x
)  ->  y  e.  B ) )
13 fpwrelmap.2 . . . . . . . 8  |-  B  e. 
_V
1413ssex 4540 . . . . . . 7  |-  ( { y  |  y  e.  ( f `  x
) }  C_  B  ->  { y  |  y  e.  ( f `  x ) }  e.  _V )
1512, 14sylbir 218 . . . . . 6  |-  ( A. y ( y  e.  ( f `  x
)  ->  y  e.  B )  ->  { y  |  y  e.  ( f `  x ) }  e.  _V )
1611, 15syl 17 . . . . 5  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  { y  |  y  e.  (
f `  x ) }  e.  _V )
173, 16opabex3d 6790 . . . 4  |-  ( f  e.  ( ~P B  ^m  A )  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  e.  _V )
1817adantl 473 . . 3  |-  ( ( T.  /\  f  e.  ( ~P B  ^m  A ) )  ->  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  e.  _V )
192mptex 6152 . . . 4  |-  ( x  e.  A  |->  { y  e.  B  |  x r y } )  e.  _V
2019a1i 11 . . 3  |-  ( ( T.  /\  r  e. 
~P ( A  X.  B ) )  -> 
( x  e.  A  |->  { y  e.  B  |  x r y } )  e.  _V )
2110imdistanda 707 . . . . . . . . . 10  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
( x  e.  A  /\  y  e.  (
f `  x )
)  ->  ( x  e.  A  /\  y  e.  B ) ) )
2221ssopab2dv 4730 . . . . . . . . 9  |-  ( f  e.  ( ~P B  ^m  A )  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) } )
2322adantr 472 . . . . . . . 8  |-  ( ( 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 468 . . . . . . . 8  |-  ( ( 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 4845 . . . . . . . . 9  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
2625a1i 11 . . . . . . . 8  |-  ( ( 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 ) } )
2723, 24, 263sstr4d 3461 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  C_  ( A  X.  B ) )
28 selpw 3949 . . . . . . 7  |-  ( r  e.  ~P ( A  X.  B )  <->  r  C_  ( A  X.  B
) )
2927, 28sylibr 217 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  e.  ~P ( A  X.  B
) )
305feqmptd 5932 . . . . . . . 8  |-  ( f  e.  ( ~P B  ^m  A )  ->  f  =  ( x  e.  A  |->  ( f `  x ) ) )
3130adantr 472 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  f  =  ( x  e.  A  |->  ( f `  x ) ) )
32 nfv 1769 . . . . . . . . 9  |-  F/ x  f  e.  ( ~P B  ^m  A )
33 nfopab1 4462 . . . . . . . . . 10  |-  F/_ x { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
3433nfeq2 2627 . . . . . . . . 9  |-  F/ x  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
3532, 34nfan 2031 . . . . . . . 8  |-  F/ x
( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
36 df-rab 2765 . . . . . . . . . 10  |-  { y  e.  B  |  x r y }  =  { y  |  ( y  e.  B  /\  x r y ) }
3736a1i 11 . . . . . . . . 9  |-  ( ( ( 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 1769 . . . . . . . . . . . 12  |-  F/ y  f  e.  ( ~P B  ^m  A )
39 nfopab2 4463 . . . . . . . . . . . . 13  |-  F/_ y { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
4039nfeq2 2627 . . . . . . . . . . . 12  |-  F/ y  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
4138, 40nfan 2031 . . . . . . . . . . 11  |-  F/ y ( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
42 nfv 1769 . . . . . . . . . . 11  |-  F/ y  x  e.  A
4341, 42nfan 2031 . . . . . . . . . 10  |-  F/ y ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  /\  x  e.  A
)
449adantllr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 4396 . . . . . . . . . . . . . . . . 17  |-  ( x r y  <->  <. x ,  y >.  e.  r
)
46 eleq2 2538 . . . . . . . . . . . . . . . . . 18  |-  ( 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 opabid 4708 . . . . . . . . . . . . . . . . . 18  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) )
4846, 47syl6bb 269 . . . . . . . . . . . . . . . . 17  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( <. x ,  y >.  e.  r  <-> 
( x  e.  A  /\  y  e.  (
f `  x )
) ) )
4945, 48syl5bb 265 . . . . . . . . . . . . . . . 16  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( x r y  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5049ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 5905 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( f `  x )  ->  x  e.  dom  f )
5251adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  dom  f )
53 fdm 5745 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : A --> ~P B  ->  dom  f  =  A )
545, 53syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( ~P B  ^m  A )  ->  dom  f  =  A )
5554adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  dom  f  =  A )
5652, 55eleqtrd 2551 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  A )
5756ex 441 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  ->  x  e.  A )
)
5857pm4.71rd 647 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5958ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) ) )
6050, 59bitr4d 264 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) )
6160biimpar 493 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
6244, 61jca 541 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
6362ex 441 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
6460biimpd 212 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) )
6564adantld 474 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
6663, 65impbid 195 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
6743, 66abbid 2588 . . . . . . . . 9  |-  ( ( ( 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 ) } )
68 abid2 2593 . . . . . . . . . 10  |-  { y  |  y  e.  ( f `  x ) }  =  ( f `
 x )
6968a1i 11 . . . . . . . . 9  |-  ( ( ( 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 ) )
7037, 67, 693eqtr2rd 2512 . . . . . . . 8  |-  ( ( ( 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 } )
7135, 70mpteq2da 4481 . . . . . . 7  |-  ( ( 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 } ) )
7231, 71eqtrd 2505 . . . . . 6  |-  ( ( 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 } ) )
7329, 72jca 541 . . . . 5  |-  ( ( 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 } ) ) )
74 ssrab2 3500 . . . . . . . . . . . 12  |-  { y  e.  B  |  x r y }  C_  B
7513elpw2 4565 . . . . . . . . . . . 12  |-  ( { y  e.  B  |  x r y }  e.  ~P B  <->  { y  e.  B  |  x
r y }  C_  B )
7674, 75mpbir 214 . . . . . . . . . . 11  |-  { y  e.  B  |  x r y }  e.  ~P B
7776a1i 11 . . . . . . . . . 10  |-  ( ( r  e.  ~P ( A  X.  B )  /\  x  e.  A )  ->  { y  e.  B  |  x r y }  e.  ~P B )
78 eqid 2471 . . . . . . . . . 10  |-  ( x  e.  A  |->  { y  e.  B  |  x r y } )  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
7977, 78fmptd 6061 . . . . . . . . 9  |-  ( r  e.  ~P ( A  X.  B )  -> 
( x  e.  A  |->  { y  e.  B  |  x r y } ) : A --> ~P B
)
8079adantr 472 . . . . . . . 8  |-  ( ( 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
)
81 simpr 468 . . . . . . . . 9  |-  ( ( 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 } ) )
8281feq1d 5724 . . . . . . . 8  |-  ( ( 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
) )
8380, 82mpbird 240 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  f : A
--> ~P B )
8413pwex 4584 . . . . . . . 8  |-  ~P B  e.  _V
8584, 2elmap 7518 . . . . . . 7  |-  ( f  e.  ( ~P B  ^m  A )  <->  f : A
--> ~P B )
8683, 85sylibr 217 . . . . . 6  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  f  e.  ( ~P B  ^m  A
) )
87 elpwi 3951 . . . . . . . . . 10  |-  ( r  e.  ~P ( A  X.  B )  -> 
r  C_  ( A  X.  B ) )
8887adantr 472 . . . . . . . . 9  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  r  C_  ( A  X.  B
) )
89 xpss 4946 . . . . . . . . 9  |-  ( A  X.  B )  C_  ( _V  X.  _V )
9088, 89syl6ss 3430 . . . . . . . 8  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  r  C_  ( _V  X.  _V )
)
91 df-rel 4846 . . . . . . . 8  |-  ( Rel  r  <->  r  C_  ( _V  X.  _V ) )
9290, 91sylibr 217 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  Rel  r )
93 relopab 4965 . . . . . . . 8  |-  Rel  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
9493a1i 11 . . . . . . 7  |-  ( ( 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 ) ) } )
95 id 22 . . . . . . 7  |-  ( ( 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 } ) ) )
96 nfv 1769 . . . . . . . . 9  |-  F/ x  r  e.  ~P ( A  X.  B )
97 nfmpt1 4485 . . . . . . . . . 10  |-  F/_ x
( x  e.  A  |->  { y  e.  B  |  x r y } )
9897nfeq2 2627 . . . . . . . . 9  |-  F/ x  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
9996, 98nfan 2031 . . . . . . . 8  |-  F/ x
( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
100 nfv 1769 . . . . . . . . 9  |-  F/ y  r  e.  ~P ( A  X.  B )
10142nfci 2602 . . . . . . . . . . 11  |-  F/_ y A
102 nfrab1 2957 . . . . . . . . . . 11  |-  F/_ y { y  e.  B  |  x r y }
103101, 102nfmpt 4484 . . . . . . . . . 10  |-  F/_ y
( x  e.  A  |->  { y  e.  B  |  x r y } )
104103nfeq2 2627 . . . . . . . . 9  |-  F/ y  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
105100, 104nfan 2031 . . . . . . . 8  |-  F/ y ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
106 nfcv 2612 . . . . . . . 8  |-  F/_ x
r
107 nfcv 2612 . . . . . . . 8  |-  F/_ y
r
108 brelg 28293 . . . . . . . . . . . . . . . 16  |-  ( ( r  C_  ( A  X.  B )  /\  x
r y )  -> 
( x  e.  A  /\  y  e.  B
) )
10987, 108sylan 479 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  ~P ( A  X.  B )  /\  x r y )  ->  ( x  e.  A  /\  y  e.  B ) )
110109adantlr 729 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) )
111110simpld 466 . . . . . . . . . . . . 13  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x  e.  A )
112110simprd 470 . . . . . . . . . . . . . 14  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  -> 
y  e.  B )
113 simpr 468 . . . . . . . . . . . . . 14  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x r y )
11481fveq1d 5881 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) )
11513rabex 4550 . . . . . . . . . . . . . . . . . . 19  |-  { y  e.  B  |  x r y }  e.  _V
11678fvmpt2 5972 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 } )
117115, 116mpan2 685 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  A  ->  (
( x  e.  A  |->  { y  e.  B  |  x r y } ) `  x )  =  { y  e.  B  |  x r y } )
118114, 117sylan9eq 2525 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 } )
119118eleq2d 2534 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 } ) )
120 rabid 2953 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { y  e.  B  |  x r y }  <->  ( y  e.  B  /\  x
r y ) )
121119, 120syl6bb 269 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
122111, 121syldan 478 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
123112, 113, 122mpbir2and 936 . . . . . . . . . . . . 13  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  -> 
y  e.  ( f `
 x ) )
124111, 123jca 541 . . . . . . . . . . . 12  |-  ( ( ( 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 )
) )
125124ex 441 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
126121simplbda 636 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
127126expl 630 . . . . . . . . . . 11  |-  ( ( 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 ) )
128125, 127impbid 195 . . . . . . . . . 10  |-  ( ( 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
) ) ) )
12945, 128syl5bbr 267 . . . . . . . . 9  |-  ( ( 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 )
) ) )
130129, 47syl6bbr 271 . . . . . . . 8  |-  ( ( 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
) ) } ) )
13199, 105, 106, 107, 33, 39, 130eqrelrd2 28298 . . . . . . 7  |-  ( ( ( 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
) ) } )
13292, 94, 95, 131syl21anc 1291 . . . . . 6  |-  ( ( 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
) ) } )
13386, 132jca 541 . . . . 5  |-  ( ( 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
) ) } ) )
13473, 133impbii 192 . . . 4  |-  ( ( 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 } ) ) )
135134a1i 11 . . 3  |-  ( 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 } ) ) ) )
1361, 18, 20, 135f1od 6538 . 2  |-  ( T. 
->  M : ( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B
) )
137136trud 1461 1  |-  M :
( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376   A.wal 1450    = wceq 1452   T. wtru 1453    e. wcel 1904   {cab 2457   {crab 2760   _Vcvv 3031    C_ wss 3390   ~Pcpw 3942   <.cop 3965   class class class wbr 4395   {copab 4453    |-> cmpt 4454    X. cxp 4837   dom cdm 4839   Rel wrel 4844   -->wf 5585   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308    ^m cmap 7490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-map 7492
This theorem is referenced by:  fpwrelmapffs  28394
  Copyright terms: Public domain W3C validator