Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brimg Unicode version

Theorem brimg 24476
Description: The binary relationship form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Hypotheses
Ref Expression
brimg.1  |-  A  e. 
_V
brimg.2  |-  B  e. 
_V
brimg.3  |-  C  e. 
_V
Assertion
Ref Expression
brimg  |-  ( <. A ,  B >.Img C  <-> 
C  =  ( A
" B ) )

Proof of Theorem brimg
Dummy variables  a 
b  p  q  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4237 . . . 4  |-  <. A ,  B >.  e.  _V
2 brimg.3 . . . 4  |-  C  e. 
_V
31, 2brco 4852 . . 3  |-  ( <. A ,  B >. (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
) C  <->  E. x
( <. A ,  B >.Cart x  /\  xImage (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C ) )
4 brimg.1 . . . . . 6  |-  A  e. 
_V
5 brimg.2 . . . . . 6  |-  B  e. 
_V
6 vex 2791 . . . . . 6  |-  x  e. 
_V
74, 5, 6brcart 24471 . . . . 5  |-  ( <. A ,  B >.Cart x  <-> 
x  =  ( A  X.  B ) )
87anbi1i 676 . . . 4  |-  ( (
<. A ,  B >.Cart x  /\  xImage ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C )  <->  ( x  =  ( A  X.  B )  /\  xImage ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C ) )
98exbii 1569 . . 3  |-  ( E. x ( <. A ,  B >.Cart x  /\  xImage ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C )  <->  E. x ( x  =  ( A  X.  B )  /\  xImage ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C ) )
104, 5xpex 4801 . . . . 5  |-  ( A  X.  B )  e. 
_V
11 breq1 4026 . . . . 5  |-  ( x  =  ( A  X.  B )  ->  (
xImage ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C  <-> 
( A  X.  B
)Image ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C ) )
1210, 11ceqsexv 2823 . . . 4  |-  ( E. x ( x  =  ( A  X.  B
)  /\  xImage (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C )  <->  ( A  X.  B )Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C )
1310, 2brimage 24465 . . . 4  |-  ( ( A  X.  B )Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C  <-> 
C  =  ( ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) " ( A  X.  B ) ) )
1412, 13bitri 240 . . 3  |-  ( E. x ( x  =  ( A  X.  B
)  /\  xImage (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) C )  <->  C  =  ( ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) "
( A  X.  B
) ) )
153, 9, 143bitri 262 . 2  |-  ( <. A ,  B >. (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
) C  <->  C  =  ( ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) "
( A  X.  B
) ) )
16 df-img 24407 . . 3  |- Img  =  (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
)
1716breqi 4029 . 2  |-  ( <. A ,  B >.Img C  <->  <. A ,  B >. (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
) C )
18 df-rex 2549 . . . . . 6  |-  ( E. y  e.  ( A  X.  B ) y ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x  <->  E. y ( y  e.  ( A  X.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )
19 elxp 4706 . . . . . . . . 9  |-  ( y  e.  ( A  X.  B )  <->  E. a E. b ( y  = 
<. a ,  b >.  /\  ( a  e.  A  /\  b  e.  B
) ) )
2019anbi1i 676 . . . . . . . 8  |-  ( ( y  e.  ( A  X.  B )  /\  y ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  ( E. a E. b ( y  = 
<. a ,  b >.  /\  ( a  e.  A  /\  b  e.  B
) )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )
21 19.41vv 1843 . . . . . . . 8  |-  ( E. a E. b ( ( y  =  <. a ,  b >.  /\  (
a  e.  A  /\  b  e.  B )
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  ( E. a E. b ( y  =  <. a ,  b
>.  /\  ( a  e.  A  /\  b  e.  B ) )  /\  y ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )
22 anass 630 . . . . . . . . 9  |-  ( ( ( y  =  <. a ,  b >.  /\  (
a  e.  A  /\  b  e.  B )
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  ( y  =  <. a ,  b
>.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
23222exbii 1570 . . . . . . . 8  |-  ( E. a E. b ( ( y  =  <. a ,  b >.  /\  (
a  e.  A  /\  b  e.  B )
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  E. a E. b ( y  = 
<. a ,  b >.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
2420, 21, 233bitr2i 264 . . . . . . 7  |-  ( ( y  e.  ( A  X.  B )  /\  y ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  E. a E. b
( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
2524exbii 1569 . . . . . 6  |-  ( E. y ( y  e.  ( A  X.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  E. y E. a E. b ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
26 excom 1786 . . . . . . 7  |-  ( E. y E. a E. b ( y  = 
<. a ,  b >.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. a E. y E. b ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
27 excom 1786 . . . . . . . . 9  |-  ( E. y E. b ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. b E. y ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) ) )
28 opex 4237 . . . . . . . . . . 11  |-  <. a ,  b >.  e.  _V
29 breq1 4026 . . . . . . . . . . . . 13  |-  ( y  =  <. a ,  b
>.  ->  ( y ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x  <->  <. a ,  b >. ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )
306brres 4961 . . . . . . . . . . . . . 14  |-  ( <.
a ,  b >.
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x  <-> 
( <. a ,  b
>. ( 2nd  o.  1st ) x  /\  <. a ,  b >.  e.  ( 1st  |`  ( _V  X.  _V ) ) ) )
31 vex 2791 . . . . . . . . . . . . . . . . 17  |-  b  e. 
_V
3231brres 4961 . . . . . . . . . . . . . . . 16  |-  ( a ( 1st  |`  ( _V  X.  _V ) ) b  <->  ( a 1st b  /\  a  e.  ( _V  X.  _V ) ) )
33 df-br 4024 . . . . . . . . . . . . . . . 16  |-  ( a ( 1st  |`  ( _V  X.  _V ) ) b  <->  <. a ,  b
>.  e.  ( 1st  |`  ( _V  X.  _V ) ) )
34 ancom 437 . . . . . . . . . . . . . . . . 17  |-  ( ( E. p E. q 
a  =  <. p ,  q >.  /\  a 1st b )  <->  ( a 1st b  /\  E. p E. q  a  =  <. p ,  q >.
) )
35 19.41vv 1843 . . . . . . . . . . . . . . . . 17  |-  ( E. p E. q ( a  =  <. p ,  q >.  /\  a 1st b )  <->  ( E. p E. q  a  = 
<. p ,  q >.  /\  a 1st b ) )
36 elvv 4748 . . . . . . . . . . . . . . . . . 18  |-  ( a  e.  ( _V  X.  _V )  <->  E. p E. q 
a  =  <. p ,  q >. )
3736anbi2i 675 . . . . . . . . . . . . . . . . 17  |-  ( ( a 1st b  /\  a  e.  ( _V  X.  _V ) )  <->  ( a 1st b  /\  E. p E. q  a  =  <. p ,  q >.
) )
3834, 35, 373bitr4ri 269 . . . . . . . . . . . . . . . 16  |-  ( ( a 1st b  /\  a  e.  ( _V  X.  _V ) )  <->  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) )
3932, 33, 383bitr3i 266 . . . . . . . . . . . . . . 15  |-  ( <.
a ,  b >.  e.  ( 1st  |`  ( _V  X.  _V ) )  <->  E. p E. q ( a  =  <. p ,  q >.  /\  a 1st b ) )
4039anbi2i 675 . . . . . . . . . . . . . 14  |-  ( (
<. a ,  b >.
( 2nd  o.  1st ) x  /\  <. a ,  b >.  e.  ( 1st  |`  ( _V  X.  _V ) ) )  <-> 
( <. a ,  b
>. ( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) )
4130, 40bitr2i 241 . . . . . . . . . . . . 13  |-  ( (
<. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) )  <->  <. a ,  b
>. ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )
4229, 41syl6bbr 254 . . . . . . . . . . . 12  |-  ( y  =  <. a ,  b
>.  ->  ( y ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x  <->  ( <. a ,  b >. ( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
4342anbi2d 684 . . . . . . . . . . 11  |-  ( y  =  <. a ,  b
>.  ->  ( ( ( a  e.  A  /\  b  e.  B )  /\  y ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )  <->  ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) ) )
4428, 43ceqsexv 2823 . . . . . . . . . 10  |-  ( E. y ( y  = 
<. a ,  b >.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  ( (
a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b
>. ( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
4544exbii 1569 . . . . . . . . 9  |-  ( E. b E. y ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. b ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
4627, 45bitri 240 . . . . . . . 8  |-  ( E. y E. b ( y  =  <. a ,  b >.  /\  (
( a  e.  A  /\  b  e.  B
)  /\  y (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. b ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
4746exbii 1569 . . . . . . 7  |-  ( E. a E. y E. b ( y  = 
<. a ,  b >.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. a E. b ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
48 an12 772 . . . . . . . . . 10  |-  ( ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  ( a  =  <. p ,  q
>.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b
>. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
49482exbii 1570 . . . . . . . . 9  |-  ( E. p E. q ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  E. p E. q ( a  = 
<. p ,  q >.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
50492exbii 1570 . . . . . . . 8  |-  ( E. a E. b E. p E. q ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  E. a E. b E. p E. q ( a  = 
<. p ,  q >.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
51 19.42vv 1848 . . . . . . . . . 10  |-  ( E. p E. q ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  ( (
( a  e.  A  /\  b  e.  B
)  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  E. p E. q ( a  =  <. p ,  q >.  /\  a 1st b ) ) )
52 anass 630 . . . . . . . . . 10  |-  ( ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) )  <->  ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
5351, 52bitri 240 . . . . . . . . 9  |-  ( E. p E. q ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  ( (
a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b
>. ( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
54532exbii 1570 . . . . . . . 8  |-  ( E. a E. b E. p E. q ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  ( a  =  <. p ,  q
>.  /\  a 1st b
) )  <->  E. a E. b ( ( a  e.  A  /\  b  e.  B )  /\  ( <. a ,  b >.
( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) ) )
55 exrot3 1818 . . . . . . . . . 10  |-  ( E. b E. p E. q ( a  = 
<. p ,  q >.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. p E. q E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
5655exbii 1569 . . . . . . . . 9  |-  ( E. a E. b E. p E. q ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. a E. p E. q E. b ( a  = 
<. p ,  q >.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
57 exrot3 1818 . . . . . . . . 9  |-  ( E. a E. p E. q E. b ( a  =  <. p ,  q
>.  /\  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b
>. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. p E. q E. a E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
58 exdistr 1847 . . . . . . . . . . . 12  |-  ( E. a E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. a
( a  =  <. p ,  q >.  /\  E. b ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b
>. ( 2nd  o.  1st ) x )  /\  a 1st b ) ) )
59 opex 4237 . . . . . . . . . . . . 13  |-  <. p ,  q >.  e.  _V
60 eleq1 2343 . . . . . . . . . . . . . . . . 17  |-  ( a  =  <. p ,  q
>.  ->  ( a  e.  A  <->  <. p ,  q
>.  e.  A ) )
6160anbi1d 685 . . . . . . . . . . . . . . . 16  |-  ( a  =  <. p ,  q
>.  ->  ( ( a  e.  A  /\  b  e.  B )  <->  ( <. p ,  q >.  e.  A  /\  b  e.  B
) ) )
62 opeq1 3796 . . . . . . . . . . . . . . . . 17  |-  ( a  =  <. p ,  q
>.  ->  <. a ,  b
>.  =  <. <. p ,  q >. ,  b
>. )
6362breq1d 4033 . . . . . . . . . . . . . . . 16  |-  ( a  =  <. p ,  q
>.  ->  ( <. a ,  b >. ( 2nd  o.  1st ) x  <->  <. <. p ,  q
>. ,  b >. ( 2nd  o.  1st )
x ) )
6461, 63anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( a  =  <. p ,  q
>.  ->  ( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b
>. ( 2nd  o.  1st ) x )  <->  ( ( <. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x ) ) )
65 breq1 4026 . . . . . . . . . . . . . . . 16  |-  ( a  =  <. p ,  q
>.  ->  ( a 1st b  <->  <. p ,  q
>. 1st b ) )
66 vex 2791 . . . . . . . . . . . . . . . . 17  |-  p  e. 
_V
67 vex 2791 . . . . . . . . . . . . . . . . 17  |-  q  e. 
_V
6866, 67, 31br1steq 24130 . . . . . . . . . . . . . . . 16  |-  ( <.
p ,  q >. 1st b  <->  b  =  p )
6965, 68syl6bb 252 . . . . . . . . . . . . . . 15  |-  ( a  =  <. p ,  q
>.  ->  ( a 1st b  <->  b  =  p ) )
7064, 69anbi12d 691 . . . . . . . . . . . . . 14  |-  ( a  =  <. p ,  q
>.  ->  ( ( ( ( a  e.  A  /\  b  e.  B
)  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b )  <->  ( (
( <. p ,  q
>.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p ) ) )
7170exbidv 1612 . . . . . . . . . . . . 13  |-  ( a  =  <. p ,  q
>.  ->  ( E. b
( ( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b )  <->  E. b
( ( ( <.
p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p ) ) )
7259, 71ceqsexv 2823 . . . . . . . . . . . 12  |-  ( E. a ( a  = 
<. p ,  q >.  /\  E. b ( ( ( a  e.  A  /\  b  e.  B
)  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. b ( ( (
<. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p ) )
7358, 72bitri 240 . . . . . . . . . . 11  |-  ( E. a E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. b
( ( ( <.
p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p ) )
74732exbii 1570 . . . . . . . . . 10  |-  ( E. p E. q E. a E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. p E. q E. b ( ( ( <. p ,  q >.  e.  A  /\  b  e.  B
)  /\  <. <. p ,  q >. ,  b
>. ( 2nd  o.  1st ) x )  /\  b  =  p )
)
75 exancom 1573 . . . . . . . . . . . 12  |-  ( E. b ( ( (
<. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p )  <->  E. b
( b  =  p  /\  ( ( <.
p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x ) ) )
76 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( b  =  p  ->  (
b  e.  B  <->  p  e.  B ) )
7776anbi2d 684 . . . . . . . . . . . . . 14  |-  ( b  =  p  ->  (
( <. p ,  q
>.  e.  A  /\  b  e.  B )  <->  ( <. p ,  q >.  e.  A  /\  p  e.  B
) ) )
78 opeq2 3797 . . . . . . . . . . . . . . 15  |-  ( b  =  p  ->  <. <. p ,  q >. ,  b
>.  =  <. <. p ,  q >. ,  p >. )
7978breq1d 4033 . . . . . . . . . . . . . 14  |-  ( b  =  p  ->  ( <. <. p ,  q
>. ,  b >. ( 2nd  o.  1st )
x  <->  <. <. p ,  q
>. ,  p >. ( 2nd  o.  1st )
x ) )
8077, 79anbi12d 691 . . . . . . . . . . . . 13  |-  ( b  =  p  ->  (
( ( <. p ,  q >.  e.  A  /\  b  e.  B
)  /\  <. <. p ,  q >. ,  b
>. ( 2nd  o.  1st ) x )  <->  ( ( <. p ,  q >.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
8166, 80ceqsexv 2823 . . . . . . . . . . . 12  |-  ( E. b ( b  =  p  /\  ( (
<. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x ) )  <->  ( ( <. p ,  q >.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
8275, 81bitri 240 . . . . . . . . . . 11  |-  ( E. b ( ( (
<. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p )  <->  ( ( <. p ,  q >.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
83822exbii 1570 . . . . . . . . . 10  |-  ( E. p E. q E. b ( ( (
<. p ,  q >.  e.  A  /\  b  e.  B )  /\  <. <.
p ,  q >. ,  b >. ( 2nd  o.  1st ) x )  /\  b  =  p )  <->  E. p E. q ( ( <.
p ,  q >.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
84 exdistr 1847 . . . . . . . . . . 11  |-  ( E. p E. q ( p  e.  B  /\  ( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )  <->  E. p ( p  e.  B  /\  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
85 an32 773 . . . . . . . . . . . . 13  |-  ( ( ( <. p ,  q
>.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  ( ( <. p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  /\  p  e.  B )
)
86 ancom 437 . . . . . . . . . . . . 13  |-  ( ( ( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  /\  p  e.  B )  <->  ( p  e.  B  /\  ( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
8785, 86bitri 240 . . . . . . . . . . . 12  |-  ( ( ( <. p ,  q
>.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  ( p  e.  B  /\  ( <. p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
88872exbii 1570 . . . . . . . . . . 11  |-  ( E. p E. q ( ( <. p ,  q
>.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  E. p E. q ( p  e.  B  /\  ( <.
p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
89 df-rex 2549 . . . . . . . . . . 11  |-  ( E. p  e.  B  E. q ( <. p ,  q >.  e.  A  /\  <. <. p ,  q
>. ,  p >. ( 2nd  o.  1st )
x )  <->  E. p
( p  e.  B  /\  E. q ( <.
p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) ) )
9084, 88, 893bitr4i 268 . . . . . . . . . 10  |-  ( E. p E. q ( ( <. p ,  q
>.  e.  A  /\  p  e.  B )  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
9174, 83, 903bitri 262 . . . . . . . . 9  |-  ( E. p E. q E. a E. b ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
9256, 57, 913bitri 262 . . . . . . . 8  |-  ( E. a E. b E. p E. q ( a  =  <. p ,  q >.  /\  (
( ( a  e.  A  /\  b  e.  B )  /\  <. a ,  b >. ( 2nd  o.  1st ) x )  /\  a 1st b ) )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
9350, 54, 923bitr3i 266 . . . . . . 7  |-  ( E. a E. b ( ( a  e.  A  /\  b  e.  B
)  /\  ( <. a ,  b >. ( 2nd  o.  1st ) x  /\  E. p E. q ( a  = 
<. p ,  q >.  /\  a 1st b ) ) )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
9426, 47, 933bitri 262 . . . . . 6  |-  ( E. y E. a E. b ( y  = 
<. a ,  b >.  /\  ( ( a  e.  A  /\  b  e.  B )  /\  y
( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x ) )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
9518, 25, 943bitri 262 . . . . 5  |-  ( E. y  e.  ( A  X.  B ) y ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x  <->  E. p  e.  B  E. q ( <. p ,  q >.  e.  A  /\  <. <. p ,  q
>. ,  p >. ( 2nd  o.  1st )
x ) )
966elima 5017 . . . . 5  |-  ( x  e.  ( ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) " ( A  X.  B ) )  <->  E. y  e.  ( A  X.  B ) y ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) x )
976elima 5017 . . . . . 6  |-  ( x  e.  ( A " B )  <->  E. p  e.  B  p A x )
98 opeq2 3797 . . . . . . . . . 10  |-  ( q  =  x  ->  <. p ,  q >.  =  <. p ,  x >. )
9998eleq1d 2349 . . . . . . . . 9  |-  ( q  =  x  ->  ( <. p ,  q >.  e.  A  <->  <. p ,  x >.  e.  A ) )
1006, 99ceqsexv 2823 . . . . . . . 8  |-  ( E. q ( q  =  x  /\  <. p ,  q >.  e.  A
)  <->  <. p ,  x >.  e.  A )
101 ancom 437 . . . . . . . . . 10  |-  ( (
<. p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  ( <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x  /\  <. p ,  q >.  e.  A
) )
102 opex 4237 . . . . . . . . . . . . 13  |-  <. <. p ,  q >. ,  p >.  e.  _V
103102, 6brco 4852 . . . . . . . . . . . 12  |-  ( <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x  <->  E. y
( <. <. p ,  q
>. ,  p >. 1st y  /\  y 2nd x ) )
104 vex 2791 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
10559, 66, 104br1steq 24130 . . . . . . . . . . . . . 14  |-  ( <. <. p ,  q >. ,  p >. 1st y  <->  y  =  <. p ,  q >.
)
106105anbi1i 676 . . . . . . . . . . . . 13  |-  ( (
<. <. p ,  q
>. ,  p >. 1st y  /\  y 2nd x )  <->  ( y  =  <. p ,  q
>.  /\  y 2nd x
) )
107106exbii 1569 . . . . . . . . . . . 12  |-  ( E. y ( <. <. p ,  q >. ,  p >. 1st y  /\  y 2nd x )  <->  E. y
( y  =  <. p ,  q >.  /\  y 2nd x ) )
108 breq1 4026 . . . . . . . . . . . . . 14  |-  ( y  =  <. p ,  q
>.  ->  ( y 2nd x  <->  <. p ,  q
>. 2nd x ) )
10959, 108ceqsexv 2823 . . . . . . . . . . . . 13  |-  ( E. y ( y  = 
<. p ,  q >.  /\  y 2nd x )  <->  <. p ,  q >. 2nd x )
11066, 67, 6br2ndeq 24131 . . . . . . . . . . . . 13  |-  ( <.
p ,  q >. 2nd x  <->  x  =  q
)
111 equcom 1647 . . . . . . . . . . . . 13  |-  ( x  =  q  <->  q  =  x )
112109, 110, 1113bitri 262 . . . . . . . . . . . 12  |-  ( E. y ( y  = 
<. p ,  q >.  /\  y 2nd x )  <-> 
q  =  x )
113103, 107, 1123bitri 262 . . . . . . . . . . 11  |-  ( <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x  <->  q  =  x )
114113anbi1i 676 . . . . . . . . . 10  |-  ( (
<. <. p ,  q
>. ,  p >. ( 2nd  o.  1st )
x  /\  <. p ,  q >.  e.  A
)  <->  ( q  =  x  /\  <. p ,  q >.  e.  A
) )
115101, 114bitri 240 . . . . . . . . 9  |-  ( (
<. p ,  q >.  e.  A  /\  <. <. p ,  q >. ,  p >. ( 2nd  o.  1st ) x )  <->  ( q  =  x  /\  <. p ,  q >.  e.  A
) )
116115exbii 1569 . . . . . . . 8  |-  ( E. q ( <. p ,  q >.  e.  A  /\  <. <. p ,  q
>. ,  p >. ( 2nd  o.  1st )
x )  <->  E. q
( q  =  x  /\  <. p ,  q
>.  e.  A ) )
117 df-br 4024 . . . . . . . 8  |-  ( p A x  <->  <. p ,  x >.  e.  A
)
118100, 116, 1173bitr4ri 269 . . . . . . 7  |-  ( p A x  <->  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
119118rexbii 2568 . . . . . 6  |-  ( E. p  e.  B  p A x  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
12097, 119bitri 240 . . . . 5  |-  ( x  e.  ( A " B )  <->  E. p  e.  B  E. q
( <. p ,  q
>.  e.  A  /\  <. <.
p ,  q >. ,  p >. ( 2nd  o.  1st ) x ) )
12195, 96, 1203bitr4ri 269 . . . 4  |-  ( x  e.  ( A " B )  <->  x  e.  ( ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) "
( A  X.  B
) ) )
122121eqriv 2280 . . 3  |-  ( A
" B )  =  ( ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) "
( A  X.  B
) )
123122eqeq2i 2293 . 2  |-  ( C  =  ( A " B )  <->  C  =  ( ( ( 2nd 
o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) ) "
( A  X.  B
) ) )
12415, 17, 1233bitr4i 268 1  |-  ( <. A ,  B >.Img C  <-> 
C  =  ( A
" B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   E.wrex 2544   _Vcvv 2788   <.cop 3643   class class class wbr 4023    X. cxp 4687    |` cres 4691   "cima 4692    o. ccom 4693   1stc1st 6120   2ndc2nd 6121  Imagecimage 24383  Cartccart 24384  Imgcimg 24385
This theorem is referenced by:  brapply  24477  dfrdg4  24488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-eprel 4305  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fo 5261  df-fv 5263  df-1st 6122  df-2nd 6123  df-symdif 24362  df-txp 24395  df-pprod 24396  df-image 24405  df-cart 24406  df-img 24407
  Copyright terms: Public domain W3C validator