Metamath Proof Explorer

Theorem xpinpreima2

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 xpinpreima2 
|- ( ( A C_ E /\ B C_ F ) -> ( A X. B ) = ( ( `' ( 1st |` ( E X. F ) ) " A ) i^i ( `' ( 2nd |` ( E X. F ) ) " B ) ) )

Proof

Step Hyp Ref Expression
1 xp2 
 |-  ( A X. B ) = { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) }
2 xpss 
 |-  ( E X. F ) C_ ( _V X. _V )
3 rabss2 
 |-  ( ( E X. F ) C_ ( _V X. _V ) -> { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } C_ { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } )
4 2 3 mp1i 
 |-  ( ( A C_ E /\ B C_ F ) -> { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } C_ { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } )
5 simprl 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> r e. ( _V X. _V ) )
6 simpll 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> A C_ E )
7 simprrl 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> ( 1st ` r ) e. A )
8 6 7 sseldd 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> ( 1st ` r ) e. E )
9 simplr 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> B C_ F )
10 simprrr 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> ( 2nd ` r ) e. B )
11 9 10 sseldd 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> ( 2nd ` r ) e. F )
12 8 11 jca 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> ( ( 1st ` r ) e. E /\ ( 2nd ` r ) e. F ) )
13 elxp7 
 |-  ( r e. ( E X. F ) <-> ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. E /\ ( 2nd ` r ) e. F ) ) )
14 5 12 13 sylanbrc 
 |-  ( ( ( A C_ E /\ B C_ F ) /\ ( r e. ( _V X. _V ) /\ ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) ) ) -> r e. ( E X. F ) )
15 14 rabss3d 
 |-  ( ( A C_ E /\ B C_ F ) -> { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } C_ { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } )
16 4 15 eqssd 
 |-  ( ( A C_ E /\ B C_ F ) -> { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } = { r e. ( _V X. _V ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } )
17 1 16 eqtr4id 
 |-  ( ( A C_ E /\ B C_ F ) -> ( A X. B ) = { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) } )
18 inrab 
 |-  ( { r e. ( E X. F ) | ( 1st ` r ) e. A } i^i { r e. ( E X. F ) | ( 2nd ` r ) e. B } ) = { r e. ( E X. F ) | ( ( 1st ` r ) e. A /\ ( 2nd ` r ) e. B ) }
19 17 18 eqtr4di 
 |-  ( ( A C_ E /\ B C_ F ) -> ( A X. B ) = ( { r e. ( E X. F ) | ( 1st ` r ) e. A } i^i { r e. ( E X. F ) | ( 2nd ` r ) e. B } ) )
20 f1stres 
 |-  ( 1st |` ( E X. F ) ) : ( E X. F ) --> E
21 ffn 
 |-  ( ( 1st |` ( E X. F ) ) : ( E X. F ) --> E -> ( 1st |` ( E X. F ) ) Fn ( E X. F ) )
22 fncnvima2 
 |-  ( ( 1st |` ( E X. F ) ) Fn ( E X. F ) -> ( `' ( 1st |` ( E X. F ) ) " A ) = { r e. ( E X. F ) | ( ( 1st |` ( E X. F ) ) ` r ) e. A } )
23 20 21 22 mp2b 
 |-  ( `' ( 1st |` ( E X. F ) ) " A ) = { r e. ( E X. F ) | ( ( 1st |` ( E X. F ) ) ` r ) e. A }
24 fvres 
 |-  ( r e. ( E X. F ) -> ( ( 1st |` ( E X. F ) ) ` r ) = ( 1st ` r ) )
25 24 eleq1d 
 |-  ( r e. ( E X. F ) -> ( ( ( 1st |` ( E X. F ) ) ` r ) e. A <-> ( 1st ` r ) e. A ) )
26 25 rabbiia 
 |-  { r e. ( E X. F ) | ( ( 1st |` ( E X. F ) ) ` r ) e. A } = { r e. ( E X. F ) | ( 1st ` r ) e. A }
27 23 26 eqtri 
 |-  ( `' ( 1st |` ( E X. F ) ) " A ) = { r e. ( E X. F ) | ( 1st ` r ) e. A }
28 f2ndres 
 |-  ( 2nd |` ( E X. F ) ) : ( E X. F ) --> F
29 ffn 
 |-  ( ( 2nd |` ( E X. F ) ) : ( E X. F ) --> F -> ( 2nd |` ( E X. F ) ) Fn ( E X. F ) )
30 fncnvima2 
 |-  ( ( 2nd |` ( E X. F ) ) Fn ( E X. F ) -> ( `' ( 2nd |` ( E X. F ) ) " B ) = { r e. ( E X. F ) | ( ( 2nd |` ( E X. F ) ) ` r ) e. B } )
31 28 29 30 mp2b 
 |-  ( `' ( 2nd |` ( E X. F ) ) " B ) = { r e. ( E X. F ) | ( ( 2nd |` ( E X. F ) ) ` r ) e. B }
32 fvres 
 |-  ( r e. ( E X. F ) -> ( ( 2nd |` ( E X. F ) ) ` r ) = ( 2nd ` r ) )
33 32 eleq1d 
 |-  ( r e. ( E X. F ) -> ( ( ( 2nd |` ( E X. F ) ) ` r ) e. B <-> ( 2nd ` r ) e. B ) )
34 33 rabbiia 
 |-  { r e. ( E X. F ) | ( ( 2nd |` ( E X. F ) ) ` r ) e. B } = { r e. ( E X. F ) | ( 2nd ` r ) e. B }
35 31 34 eqtri 
 |-  ( `' ( 2nd |` ( E X. F ) ) " B ) = { r e. ( E X. F ) | ( 2nd ` r ) e. B }
36 27 35 ineq12i 
 |-  ( ( `' ( 1st |` ( E X. F ) ) " A ) i^i ( `' ( 2nd |` ( E X. F ) ) " B ) ) = ( { r e. ( E X. F ) | ( 1st ` r ) e. A } i^i { r e. ( E X. F ) | ( 2nd ` r ) e. B } )
37 19 36 eqtr4di 
 |-  ( ( A C_ E /\ B C_ F ) -> ( A X. B ) = ( ( `' ( 1st |` ( E X. F ) ) " A ) i^i ( `' ( 2nd |` ( E X. F ) ) " B ) ) )