Metamath Proof Explorer

Theorem xpinpreima

Description: Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017)

Ref Expression
Assertion xpinpreima 
|- ( A X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) " A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) " B ) )

Proof

Step Hyp Ref Expression
1 inrab 
 |-  ( { r e. ( _V X. _V ) | ( 1st ` r ) e. A } i^i { r e. ( _V X. _V ) | ( 2nd ` r ) e. B } ) = { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) }
2 f1stres 
 |-  ( 1st |` ( _V X. _V ) ) : ( _V X. _V ) --> _V
3 ffn 
 |-  ( ( 1st |` ( _V X. _V ) ) : ( _V X. _V ) --> _V -> ( 1st |` ( _V X. _V ) ) Fn ( _V X. _V ) )
4 fncnvima2 
 |-  ( ( 1st |` ( _V X. _V ) ) Fn ( _V X. _V ) -> ( `' ( 1st |` ( _V X. _V ) ) " A ) = { r e. ( _V X. _V ) | ( ( 1st |` ( _V X. _V ) ) ` r ) e. A } )
5 2 3 4 mp2b 
 |-  ( `' ( 1st |` ( _V X. _V ) ) " A ) = { r e. ( _V X. _V ) | ( ( 1st |` ( _V X. _V ) ) ` r ) e. A }
6 fvres 
 |-  ( r e. ( _V X. _V ) -> ( ( 1st |` ( _V X. _V ) ) ` r ) = ( 1st ` r ) )
7 6 eleq1d 
 |-  ( r e. ( _V X. _V ) -> ( ( ( 1st |` ( _V X. _V ) ) ` r ) e. A <-> ( 1st ` r ) e. A ) )
8 7 rabbiia 
 |-  { r e. ( _V X. _V ) | ( ( 1st |` ( _V X. _V ) ) ` r ) e. A } = { r e. ( _V X. _V ) | ( 1st ` r ) e. A }
9 5 8 eqtri 
 |-  ( `' ( 1st |` ( _V X. _V ) ) " A ) = { r e. ( _V X. _V ) | ( 1st ` r ) e. A }
10 f2ndres 
 |-  ( 2nd |` ( _V X. _V ) ) : ( _V X. _V ) --> _V
11 ffn 
 |-  ( ( 2nd |` ( _V X. _V ) ) : ( _V X. _V ) --> _V -> ( 2nd |` ( _V X. _V ) ) Fn ( _V X. _V ) )
12 fncnvima2 
 |-  ( ( 2nd |` ( _V X. _V ) ) Fn ( _V X. _V ) -> ( `' ( 2nd |` ( _V X. _V ) ) " B ) = { r e. ( _V X. _V ) | ( ( 2nd |` ( _V X. _V ) ) ` r ) e. B } )
13 10 11 12 mp2b 
 |-  ( `' ( 2nd |` ( _V X. _V ) ) " B ) = { r e. ( _V X. _V ) | ( ( 2nd |` ( _V X. _V ) ) ` r ) e. B }
14 fvres 
 |-  ( r e. ( _V X. _V ) -> ( ( 2nd |` ( _V X. _V ) ) ` r ) = ( 2nd ` r ) )
15 14 eleq1d 
 |-  ( r e. ( _V X. _V ) -> ( ( ( 2nd |` ( _V X. _V ) ) ` r ) e. B <-> ( 2nd ` r ) e. B ) )
16 15 rabbiia 
 |-  { r e. ( _V X. _V ) | ( ( 2nd |` ( _V X. _V ) ) ` r ) e. B } = { r e. ( _V X. _V ) | ( 2nd ` r ) e. B }
17 13 16 eqtri 
 |-  ( `' ( 2nd |` ( _V X. _V ) ) " B ) = { r e. ( _V X. _V ) | ( 2nd ` r ) e. B }
18 9 17 ineq12i 
 |-  ( ( `' ( 1st |` ( _V X. _V ) ) " A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) " B ) ) = ( { r e. ( _V X. _V ) | ( 1st ` r ) e. A } i^i { r e. ( _V X. _V ) | ( 2nd ` r ) e. B } )
19 xp2 
 |-  ( A X. B ) = { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) }
20 1 18 19 3eqtr4ri 
 |-  ( A X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) " A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) " B ) )