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

Theorem fpwrelmap 27706
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 8741 and marypha2lem1 7810. (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 459 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  ( f `  x
) )
5 elmapi 7359 . . . . . . . . . . 11  |-  ( f  e.  ( ~P B  ^m  A )  ->  f : A --> ~P B )
65ffvelrnda 5933 . . . . . . . . . 10  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( f `  x )  e.  ~P B )
76adantr 463 . . . . . . . . 9  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  (
f `  x )  e.  ~P B )
8 elelpwi 3938 . . . . . . . . 9  |-  ( ( y  e.  ( f `
 x )  /\  ( f `  x
)  e.  ~P B
)  ->  y  e.  B )
94, 7, 8syl2anc 659 . . . . . . . 8  |-  ( ( ( f  e.  ( ~P B  ^m  A
)  /\  x  e.  A )  /\  y  e.  ( f `  x
) )  ->  y  e.  B )
109ex 432 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  ( y  e.  ( f `  x
)  ->  y  e.  B ) )
1110alrimiv 1727 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  A. y
( y  e.  ( f `  x )  ->  y  e.  B
) )
12 abss 3483 . . . . . . 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 4509 . . . . . . 7  |-  ( { y  |  y  e.  ( f `  x
) }  C_  B  ->  { y  |  y  e.  ( f `  x ) }  e.  _V )
1512, 14sylbir 213 . . . . . 6  |-  ( A. y ( y  e.  ( f `  x
)  ->  y  e.  B )  ->  { y  |  y  e.  ( f `  x ) }  e.  _V )
1611, 15syl 16 . . . . 5  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  x  e.  A
)  ->  { y  |  y  e.  (
f `  x ) }  e.  _V )
173, 16opabex3d 6677 . . . 4  |-  ( f  e.  ( ~P B  ^m  A )  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  e.  _V )
1817adantl 464 . . 3  |-  ( ( T.  /\  f  e.  ( ~P B  ^m  A ) )  ->  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  e.  _V )
192mptex 6044 . . . 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 691 . . . . . . . . . 10  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
( x  e.  A  /\  y  e.  (
f `  x )
)  ->  ( x  e.  A  /\  y  e.  B ) ) )
2221ssopab2dv 4690 . . . . . . . . 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 463 . . . . . . . 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 459 . . . . . . . 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 4919 . . . . . . . . 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 3460 . . . . . . 7  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  C_  ( A  X.  B ) )
28 selpw 3934 . . . . . . 7  |-  ( r  e.  ~P ( A  X.  B )  <->  r  C_  ( A  X.  B
) )
2927, 28sylibr 212 . . . . . 6  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  ->  r  e.  ~P ( A  X.  B
) )
305feqmptd 5827 . . . . . . . 8  |-  ( f  e.  ( ~P B  ^m  A )  ->  f  =  ( x  e.  A  |->  ( f `  x ) ) )
3130adantr 463 . . . . . . 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 1715 . . . . . . . . 9  |-  F/ x  f  e.  ( ~P B  ^m  A )
33 nfopab1 4433 . . . . . . . . . 10  |-  F/_ x { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
3433nfeq2 2561 . . . . . . . . 9  |-  F/ x  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
3532, 34nfan 1936 . . . . . . . 8  |-  F/ x
( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
36 df-rab 2741 . . . . . . . . . 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 1715 . . . . . . . . . . . 12  |-  F/ y  f  e.  ( ~P B  ^m  A )
39 nfopab2 4434 . . . . . . . . . . . . 13  |-  F/_ y { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }
4039nfeq2 2561 . . . . . . . . . . . 12  |-  F/ y  r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }
4138, 40nfan 1936 . . . . . . . . . . 11  |-  F/ y ( f  e.  ( ~P B  ^m  A
)  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )
42 nfv 1715 . . . . . . . . . . 11  |-  F/ y  x  e.  A
4341, 42nfan 1936 . . . . . . . . . 10  |-  F/ y ( ( f  e.  ( ~P B  ^m  A )  /\  r  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) } )  /\  x  e.  A
)
449adantllr 716 . . . . . . . . . . . . 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 4368 . . . . . . . . . . . . . . . . 17  |-  ( x r y  <->  <. x ,  y >.  e.  r
)
46 eleq2 2455 . . . . . . . . . . . . . . . . . 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 4668 . . . . . . . . . . . . . . . . . 18  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( f `  x
) ) }  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) )
4846, 47syl6bb 261 . . . . . . . . . . . . . . . . 17  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( <. x ,  y >.  e.  r  <-> 
( x  e.  A  /\  y  e.  (
f `  x )
) ) )
4945, 48syl5bb 257 . . . . . . . . . . . . . . . 16  |-  ( r  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( f `  x ) ) }  ->  ( x r y  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5049ad2antlr 724 . . . . . . . . . . . . . . 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 5800 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( f `  x )  ->  x  e.  dom  f )
5251adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  dom  f )
53 fdm 5643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : A --> ~P B  ->  dom  f  =  A )
545, 53syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  e.  ( ~P B  ^m  A )  ->  dom  f  =  A )
5554adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  dom  f  =  A )
5652, 55eleqtrd 2472 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  e.  ( ~P B  ^m  A )  /\  y  e.  ( f `  x ) )  ->  x  e.  A )
5756ex 432 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  ->  x  e.  A )
)
5857pm4.71rd 633 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( ~P B  ^m  A )  ->  (
y  e.  ( f `
 x )  <->  ( x  e.  A  /\  y  e.  ( f `  x
) ) ) )
5958ad2antrr 723 . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . 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 530 . . . . . . . . . . . 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 432 . . . . . . . . . . 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 207 . . . . . . . . . . . 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 465 . . . . . . . . . . 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 191 . . . . . . . . . 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 2517 . . . . . . . . 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 2522 . . . . . . . . . 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 2430 . . . . . . . 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 4452 . . . . . . 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 2423 . . . . . 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 530 . . . . 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 3499 . . . . . . . . . . . 12  |-  { y  e.  B  |  x r y }  C_  B
7513elpw2 4529 . . . . . . . . . . . 12  |-  ( { y  e.  B  |  x r y }  e.  ~P B  <->  { y  e.  B  |  x
r y }  C_  B )
7674, 75mpbir 209 . . . . . . . . . . 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 2382 . . . . . . . . . 10  |-  ( x  e.  A  |->  { y  e.  B  |  x r y } )  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
7977, 78fmptd 5957 . . . . . . . . 9  |-  ( r  e.  ~P ( A  X.  B )  -> 
( x  e.  A  |->  { y  e.  B  |  x r y } ) : A --> ~P B
)
8079adantr 463 . . . . . . . 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 459 . . . . . . . . 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 5625 . . . . . . . 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 232 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  f : A
--> ~P B )
8413pwex 4548 . . . . . . . 8  |-  ~P B  e.  _V
8584, 2elmap 7366 . . . . . . 7  |-  ( f  e.  ( ~P B  ^m  A )  <->  f : A
--> ~P B )
8683, 85sylibr 212 . . . . . 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 3936 . . . . . . . . . 10  |-  ( r  e.  ~P ( A  X.  B )  -> 
r  C_  ( A  X.  B ) )
8887adantr 463 . . . . . . . . 9  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  r  C_  ( A  X.  B
) )
89 xpss 5022 . . . . . . . . 9  |-  ( A  X.  B )  C_  ( _V  X.  _V )
9088, 89syl6ss 3429 . . . . . . . 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 4920 . . . . . . . 8  |-  ( Rel  r  <->  r  C_  ( _V  X.  _V ) )
9290, 91sylibr 212 . . . . . . 7  |-  ( ( r  e.  ~P ( A  X.  B )  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  ->  Rel  r )
93 relopab 5041 . . . . . . . 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 1715 . . . . . . . . 9  |-  F/ x  r  e.  ~P ( A  X.  B )
97 nfmpt1 4456 . . . . . . . . . 10  |-  F/_ x
( x  e.  A  |->  { y  e.  B  |  x r y } )
9897nfeq2 2561 . . . . . . . . 9  |-  F/ x  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
9996, 98nfan 1936 . . . . . . . 8  |-  F/ x
( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
100 nfv 1715 . . . . . . . . 9  |-  F/ y  r  e.  ~P ( A  X.  B )
10142nfci 2533 . . . . . . . . . . 11  |-  F/_ y A
102 nfrab1 2963 . . . . . . . . . . 11  |-  F/_ y { y  e.  B  |  x r y }
103101, 102nfmpt 4455 . . . . . . . . . 10  |-  F/_ y
( x  e.  A  |->  { y  e.  B  |  x r y } )
104103nfeq2 2561 . . . . . . . . 9  |-  F/ y  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } )
105100, 104nfan 1936 . . . . . . . 8  |-  F/ y ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )
106 nfcv 2544 . . . . . . . 8  |-  F/_ x
r
107 nfcv 2544 . . . . . . . 8  |-  F/_ y
r
108 brelg 27596 . . . . . . . . . . . . . . . 16  |-  ( ( r  C_  ( A  X.  B )  /\  x
r y )  -> 
( x  e.  A  /\  y  e.  B
) )
10987, 108sylan 469 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  ~P ( A  X.  B )  /\  x r y )  ->  ( x  e.  A  /\  y  e.  B ) )
110109adantlr 712 . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . 13  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x  e.  A )
112110simprd 461 . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . 14  |-  ( ( ( r  e.  ~P ( A  X.  B
)  /\  f  =  ( x  e.  A  |->  { y  e.  B  |  x r y } ) )  /\  x
r y )  ->  x r y )
11481fveq1d 5776 . . . . . . . . . . . . . . . . . 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 4516 . . . . . . . . . . . . . . . . . . 19  |-  { y  e.  B  |  x r y }  e.  _V
11678fvmpt2 5865 . . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  A  ->  (
( x  e.  A  |->  { y  e.  B  |  x r y } ) `  x )  =  { y  e.  B  |  x r y } )
118114, 117sylan9eq 2443 . . . . . . . . . . . . . . . . 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 2452 . . . . . . . . . . . . . . . 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 2959 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { y  e.  B  |  x r y }  <->  ( y  e.  B  /\  x
r y ) )
121119, 120syl6bb 261 . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 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 920 . . . . . . . . . . . . 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 530 . . . . . . . . . . . 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 432 . . . . . . . . . . 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 622 . . . . . . . . . . . 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 616 . . . . . . . . . . 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 191 . . . . . . . . . 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 259 . . . . . . . . 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 263 . . . . . . . 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 27601 . . . . . . 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 1225 . . . . . 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 530 . . . . 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 188 . . . 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 6424 . 2  |-  ( T. 
->  M : ( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B
) )
137136trud 1408 1  |-  M :
( ~P B  ^m  A ) -1-1-onto-> ~P ( A  X.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1397    = wceq 1399   T. wtru 1400    e. wcel 1826   {cab 2367   {crab 2736   _Vcvv 3034    C_ wss 3389   ~Pcpw 3927   <.cop 3950   class class class wbr 4367   {copab 4424    |-> cmpt 4425    X. cxp 4911   dom cdm 4913   Rel wrel 4918   -->wf 5492   -1-1-onto->wf1o 5495   ` cfv 5496  (class class class)co 6196    ^m cmap 7338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-1st 6699  df-2nd 6700  df-map 7340
This theorem is referenced by:  fpwrelmapffs  27707
  Copyright terms: Public domain W3C validator