Metamath Proof Explorer

Theorem xppreima2

Description: The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017)

Ref Expression
Hypotheses xppreima2.1 
|- ( ph -> F : A --> B )
xppreima2.2 
|- ( ph -> G : A --> C )
xppreima2.3 
|- H = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. )
Assertion xppreima2 
|- ( ph -> ( `' H " ( Y X. Z ) ) = ( ( `' F " Y ) i^i ( `' G " Z ) ) )

Proof

Step Hyp Ref Expression
1 xppreima2.1 
 |-  ( ph -> F : A --> B )
2 xppreima2.2 
 |-  ( ph -> G : A --> C )
3 xppreima2.3 
 |-  H = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. )
4 3 funmpt2 
 |-  Fun H
5 1 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
6 2 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. C )
7 opelxp 
 |-  ( <. ( F ` x ) , ( G ` x ) >. e. ( B X. C ) <-> ( ( F ` x ) e. B /\ ( G ` x ) e. C ) )
8 5 6 7 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> <. ( F ` x ) , ( G ` x ) >. e. ( B X. C ) )
9 8 3 fmptd 
 |-  ( ph -> H : A --> ( B X. C ) )
10 9 frnd 
 |-  ( ph -> ran H C_ ( B X. C ) )
11 xpss 
 |-  ( B X. C ) C_ ( _V X. _V )
12 10 11 sstrdi 
 |-  ( ph -> ran H C_ ( _V X. _V ) )
13 xppreima 
 |-  ( ( Fun H /\ ran H C_ ( _V X. _V ) ) -> ( `' H " ( Y X. Z ) ) = ( ( `' ( 1st o. H ) " Y ) i^i ( `' ( 2nd o. H ) " Z ) ) )
14 4 12 13 sylancr 
 |-  ( ph -> ( `' H " ( Y X. Z ) ) = ( ( `' ( 1st o. H ) " Y ) i^i ( `' ( 2nd o. H ) " Z ) ) )
15 fo1st 
 |-  1st : _V -onto-> _V
16 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
17 15 16 ax-mp 
 |-  1st Fn _V
18 opex 
 |-  <. ( F ` x ) , ( G ` x ) >. e. _V
19 18 3 fnmpti 
 |-  H Fn A
20 ssv 
 |-  ran H C_ _V
21 fnco 
 |-  ( ( 1st Fn _V /\ H Fn A /\ ran H C_ _V ) -> ( 1st o. H ) Fn A )
22 17 19 20 21 mp3an 
 |-  ( 1st o. H ) Fn A
23 22 a1i 
 |-  ( ph -> ( 1st o. H ) Fn A )
24 1 ffnd 
 |-  ( ph -> F Fn A )
25 4 a1i 
 |-  ( ( ph /\ x e. A ) -> Fun H )
26 12 adantr 
 |-  ( ( ph /\ x e. A ) -> ran H C_ ( _V X. _V ) )
27 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
28 18 3 dmmpti 
 |-  dom H = A
29 27 28 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> x e. dom H )
30 opfv 
 |-  ( ( ( Fun H /\ ran H C_ ( _V X. _V ) ) /\ x e. dom H ) -> ( H ` x ) = <. ( ( 1st o. H ) ` x ) , ( ( 2nd o. H ) ` x ) >. )
31 25 26 29 30 syl21anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = <. ( ( 1st o. H ) ` x ) , ( ( 2nd o. H ) ` x ) >. )
32 3 fvmpt2 
 |-  ( ( x e. A /\ <. ( F ` x ) , ( G ` x ) >. e. ( B X. C ) ) -> ( H ` x ) = <. ( F ` x ) , ( G ` x ) >. )
33 27 8 32 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = <. ( F ` x ) , ( G ` x ) >. )
34 31 33 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> <. ( ( 1st o. H ) ` x ) , ( ( 2nd o. H ) ` x ) >. = <. ( F ` x ) , ( G ` x ) >. )
35 fvex 
 |-  ( ( 1st o. H ) ` x ) e. _V
36 fvex 
 |-  ( ( 2nd o. H ) ` x ) e. _V
37 35 36 opth 
 |-  ( <. ( ( 1st o. H ) ` x ) , ( ( 2nd o. H ) ` x ) >. = <. ( F ` x ) , ( G ` x ) >. <-> ( ( ( 1st o. H ) ` x ) = ( F ` x ) /\ ( ( 2nd o. H ) ` x ) = ( G ` x ) ) )
38 34 37 sylib 
 |-  ( ( ph /\ x e. A ) -> ( ( ( 1st o. H ) ` x ) = ( F ` x ) /\ ( ( 2nd o. H ) ` x ) = ( G ` x ) ) )
39 38 simpld 
 |-  ( ( ph /\ x e. A ) -> ( ( 1st o. H ) ` x ) = ( F ` x ) )
40 23 24 39 eqfnfvd 
 |-  ( ph -> ( 1st o. H ) = F )
41 40 cnveqd 
 |-  ( ph -> `' ( 1st o. H ) = `' F )
42 41 imaeq1d 
 |-  ( ph -> ( `' ( 1st o. H ) " Y ) = ( `' F " Y ) )
43 fo2nd 
 |-  2nd : _V -onto-> _V
44 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
45 43 44 ax-mp 
 |-  2nd Fn _V
46 fnco 
 |-  ( ( 2nd Fn _V /\ H Fn A /\ ran H C_ _V ) -> ( 2nd o. H ) Fn A )
47 45 19 20 46 mp3an 
 |-  ( 2nd o. H ) Fn A
48 47 a1i 
 |-  ( ph -> ( 2nd o. H ) Fn A )
49 2 ffnd 
 |-  ( ph -> G Fn A )
50 38 simprd 
 |-  ( ( ph /\ x e. A ) -> ( ( 2nd o. H ) ` x ) = ( G ` x ) )
51 48 49 50 eqfnfvd 
 |-  ( ph -> ( 2nd o. H ) = G )
52 51 cnveqd 
 |-  ( ph -> `' ( 2nd o. H ) = `' G )
53 52 imaeq1d 
 |-  ( ph -> ( `' ( 2nd o. H ) " Z ) = ( `' G " Z ) )
54 42 53 ineq12d 
 |-  ( ph -> ( ( `' ( 1st o. H ) " Y ) i^i ( `' ( 2nd o. H ) " Z ) ) = ( ( `' F " Y ) i^i ( `' G " Z ) ) )
55 14 54 eqtrd 
 |-  ( ph -> ( `' H " ( Y X. Z ) ) = ( ( `' F " Y ) i^i ( `' G " Z ) ) )