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 28311
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 8875 and marypha2lem1 7946. (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 463 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  ( f `  x
) )
5 elmapi 7490 . . . . . . . . . . 11  |-  ( f  e.  ( ~P B  ^m  A )  ->  f : A --> ~P B )
65ffvelrnda 6020 . . . . . . . . . 10  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( f `  x )  e.  ~P B )
76adantr 467 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  (
f `  x )  e.  ~P B )
8 elelpwi 3961 . . . . . . . . 9  |-  ( ( y  e.  ( f `
 x )  /\  ( f `  x
)  e.  ~P B
)  ->  y  e.  B )
94, 7, 8syl2anc 666 . . . . . . . 8  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  B )
109ex 436 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( y  e.  ( f `  x
)  ->  y  e.  B ) )
1110alrimiv 1772 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  A. y
( y  e.  ( f `  x )  ->  y  e.  B
) )
12 abss 3497 . . . . . . 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 4546 . . . . . . 7  |-  ( { y  |  y  e.  ( f `  x
) }  C_  B  ->  { y  |  y  e.  ( f `  x ) }  e.  _V )
1512, 14sylbir 217 . . . . . 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 6768 . . . 4  |-  ( f  e.  ( ~P B  ^m  A )  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  e.  _V )
1817adantl 468 . . 3  |-  ( ( T.  /\  f  e.  ( ~P B  ^m  A ) )  ->  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  e.  _V )
192mptex 6134 . . . 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 698 . . . . . . . . . 10  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
( x  e.  A  /\  y  e.  (
f `  x )
)  ->  ( x  e.  A  /\  y  e.  B ) ) )
2221ssopab2dv 4729 . . . . . . . . 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 467 . . . . . . . 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 463 . . . . . . . 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 4839 . . . . . . . . 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 3474 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  C_  ( A  X.  B ) )
28 selpw 3957 . . . . . . 7  |-  ( r  e.  ~P ( A  X.  B )  <->  r  C_  ( A  X.  B
) )
2927, 28sylibr 216 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  e.  ~P ( A  X.  B
) )
305feqmptd 5916 . . . . . . . 8  |-  ( f  e.  ( ~P B  ^m  A )  ->  f  =  ( x  e.  A  |->  ( f `  x ) ) )
3130adantr 467 . . . . . . 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 1760 . . . . . . . . 9  |-  F/ x  f  e.  ( ~P B  ^m  A )
33 nfopab1 4468 . . . . . . . . . 10  |-  F/_ x { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
3433nfeq2 2606 . . . . . . . . 9  |-  F/ x  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
3532, 34nfan 2010 . . . . . . . 8  |-  F/ x
( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
36 df-rab 2745 . . . . . . . . . 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 1760 . . . . . . . . . . . 12  |-  F/ y  f  e.  ( ~P B  ^m  A )
39 nfopab2 4469 . . . . . . . . . . . . 13  |-  F/_ y { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
4039nfeq2 2606 . . . . . . . . . . . 12  |-  F/ y  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
4138, 40nfan 2010 . . . . . . . . . . 11  |-  F/ y ( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
42 nfv 1760 . . . . . . . . . . 11  |-  F/ y  x  e.  A
4341, 42nfan 2010 . . . . . . . . . 10  |-  F/ y ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  /\  x  e.  A
)
449adantllr 724 . . . . . . . . . . . . 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 4402 . . . . . . . . . . . . . . . . 17  |-  ( x r y  <->  <. x ,  y >.  e.  r
)
46 eleq2 2517 . . . . . . . . . . . . . . . . . 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 4707 . . . . . . . . . . . . . . . . . 18  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) )
4846, 47syl6bb 265 . . . . . . . . . . . . . . . . 17  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( <. x ,  y >.  e.  r  <-> 
( x  e.  A  /\  y  e.  (
f `  x )
) ) )
4945, 48syl5bb 261 . . . . . . . . . . . . . . . 16  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( x r y  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5049ad2antlr 732 . . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( f `  x )  ->  x  e.  dom  f )
5251adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  dom  f )
53 fdm 5731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : A --> ~P B  ->  dom  f  =  A )
545, 53syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( ~P B  ^m  A )  ->  dom  f  =  A )
5554adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  dom  f  =  A )
5652, 55eleqtrd 2530 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  A )
5756ex 436 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  ->  x  e.  A )
)
5857pm4.71rd 640 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5958ad2antrr 731 . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . 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 535 . . . . . . . . . . . 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 436 . . . . . . . . . . 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 211 . . . . . . . . . . . 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 469 . . . . . . . . . . 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 194 . . . . . . . . . 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 2567 . . . . . . . . 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 2572 . . . . . . . . . 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 2491 . . . . . . . 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 4487 . . . . . . 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 2484 . . . . . 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 535 . . . . 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 3513 . . . . . . . . . . . 12  |-  { y  e.  B  |  x r y }  C_  B
7513elpw2 4566 . . . . . . . . . . . 12  |-  ( { y  e.  B  |  x r y }  e.  ~P B  <->  { y  e.  B  |  x
r y }  C_  B )
7674, 75mpbir 213 . . . . . . . . . . 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 2450 . . . . . . . . . 10  |-  ( x  e.  A  |->  { y  e.  B  |  x r y } )  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
7977, 78fmptd 6044 . . . . . . . . 9  |-  ( r  e.  ~P ( A  X.  B )  -> 
( x  e.  A  |->  { y  e.  B  |  x r y } ) : A --> ~P B
)
8079adantr 467 . . . . . . . 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 463 . . . . . . . . 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 5712 . . . . . . . 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 236 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  f : A
--> ~P B )
8413pwex 4585 . . . . . . . 8  |-  ~P B  e.  _V
8584, 2elmap 7497 . . . . . . 7  |-  ( f  e.  ( ~P B  ^m  A )  <->  f : A
--> ~P B )
8683, 85sylibr 216 . . . . . 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 3959 . . . . . . . . . 10  |-  ( r  e.  ~P ( A  X.  B )  -> 
r  C_  ( A  X.  B ) )
8887adantr 467 . . . . . . . . 9  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  r  C_  ( A  X.  B
) )
89 xpss 4940 . . . . . . . . 9  |-  ( A  X.  B )  C_  ( _V  X.  _V )
9088, 89syl6ss 3443 . . . . . . . 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 4840 . . . . . . . 8  |-  ( Rel  r  <->  r  C_  ( _V  X.  _V ) )
9290, 91sylibr 216 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  Rel  r )
93 relopab 4959 . . . . . . . 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 1760 . . . . . . . . 9  |-  F/ x  r  e.  ~P ( A  X.  B )
97 nfmpt1 4491 . . . . . . . . . 10  |-  F/_ x
( x  e.  A  |->  { y  e.  B  |  x r y } )
9897nfeq2 2606 . . . . . . . . 9  |-  F/ x  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
9996, 98nfan 2010 . . . . . . . 8  |-  F/ x
( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
100 nfv 1760 . . . . . . . . 9  |-  F/ y  r  e.  ~P ( A  X.  B )
10142nfci 2581 . . . . . . . . . . 11  |-  F/_ y A
102 nfrab1 2970 . . . . . . . . . . 11  |-  F/_ y { y  e.  B  |  x r y }
103101, 102nfmpt 4490 . . . . . . . . . 10  |-  F/_ y
( x  e.  A  |->  { y  e.  B  |  x r y } )
104103nfeq2 2606 . . . . . . . . 9  |-  F/ y  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
105100, 104nfan 2010 . . . . . . . 8  |-  F/ y ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
106 nfcv 2591 . . . . . . . 8  |-  F/_ x
r
107 nfcv 2591 . . . . . . . 8  |-  F/_ y
r
108 brelg 28210 . . . . . . . . . . . . . . . 16  |-  ( ( r  C_  ( A  X.  B )  /\  x
r y )  -> 
( x  e.  A  /\  y  e.  B
) )
10987, 108sylan 474 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  ~P ( A  X.  B )  /\  x r y )  ->  ( x  e.  A  /\  y  e.  B ) )
110109adantlr 720 . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . 13  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x  e.  A )
112110simprd 465 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 14  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x r y )
11481fveq1d 5865 . . . . . . . . . . . . . . . . . 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 4553 . . . . . . . . . . . . . . . . . . 19  |-  { y  e.  B  |  x r y }  e.  _V
11678fvmpt2 5955 . . . . . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  A  ->  (
( x  e.  A  |->  { y  e.  B  |  x r y } ) `  x )  =  { y  e.  B  |  x r y } )
118114, 117sylan9eq 2504 . . . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . . . . 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 2966 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { y  e.  B  |  x r y }  <->  ( y  e.  B  /\  x
r y ) )
121119, 120syl6bb 265 . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . 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 932 . . . . . . . . . . . . 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 535 . . . . . . . . . . . 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 436 . . . . . . . . . . 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 629 . . . . . . . . . . . 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 623 . . . . . . . . . . 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 194 . . . . . . . . . 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 263 . . . . . . . . 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 267 . . . . . . . 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 28215 . . . . . . 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 1266 . . . . . 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 535 . . . . 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 191 . . . 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 6516 . 2  |-  ( T. 
->  M : ( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B
) )
137136trud 1452 1  |-  M :
( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1441    = wceq 1443   T. wtru 1444    e. wcel 1886   {cab 2436   {crab 2740   _Vcvv 3044    C_ wss 3403   ~Pcpw 3950   <.cop 3973   class class class wbr 4401   {copab 4459    |-> cmpt 4460    X. cxp 4831   dom cdm 4833   Rel wrel 4838   -->wf 5577   -1-1-onto->wf1o 5580   ` cfv 5581  (class class class)co 6288    ^m cmap 7469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-map 7471
This theorem is referenced by:  fpwrelmapffs  28312
  Copyright terms: Public domain W3C validator