This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xppreima

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

Ref Expression
Assertion xppreima 
|- ( ( Fun F /\ ran F C_ ( _V X. _V ) ) -> ( `' F " ( Y X. Z ) ) = ( ( `' ( 1st o. F ) " Y ) i^i ( `' ( 2nd o. F ) " Z ) ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 fncnvima2 
 |-  ( F Fn dom F -> ( `' F " ( Y X. Z ) ) = { x e. dom F | ( F ` x ) e. ( Y X. Z ) } )
3 1 2 sylbi 
 |-  ( Fun F -> ( `' F " ( Y X. Z ) ) = { x e. dom F | ( F ` x ) e. ( Y X. Z ) } )
4 3 adantr 
 |-  ( ( Fun F /\ ran F C_ ( _V X. _V ) ) -> ( `' F " ( Y X. Z ) ) = { x e. dom F | ( F ` x ) e. ( Y X. Z ) } )
5 elxp6 
 |-  ( ( F ` x ) e. ( Y X. Z ) <-> ( ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. /\ ( ( 1st ` ( F ` x ) ) e. Y /\ ( 2nd ` ( F ` x ) ) e. Z ) ) )
6 fvco 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( 1st o. F ) ` x ) = ( 1st ` ( F ` x ) ) )
7 fvco 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( 2nd o. F ) ` x ) = ( 2nd ` ( F ` x ) ) )
8 6 7 opeq12d 
 |-  ( ( Fun F /\ x e. dom F ) -> <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
9 8 eqeq2d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. <-> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
10 6 eleq1d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( 1st o. F ) ` x ) e. Y <-> ( 1st ` ( F ` x ) ) e. Y ) )
11 7 eleq1d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( 2nd o. F ) ` x ) e. Z <-> ( 2nd ` ( F ` x ) ) e. Z ) )
12 10 11 anbi12d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) <-> ( ( 1st ` ( F ` x ) ) e. Y /\ ( 2nd ` ( F ` x ) ) e. Z ) ) )
13 9 12 anbi12d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. /\ ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) ) <-> ( ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. /\ ( ( 1st ` ( F ` x ) ) e. Y /\ ( 2nd ` ( F ` x ) ) e. Z ) ) ) )
14 5 13 bitr4id 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) e. ( Y X. Z ) <-> ( ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. /\ ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) ) ) )
15 14 adantlr 
 |-  ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( ( F ` x ) e. ( Y X. Z ) <-> ( ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. /\ ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) ) ) )
16 opfv 
 |-  ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. )
17 16 biantrurd 
 |-  ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) <-> ( ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. /\ ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) ) ) )
18 fo1st 
 |-  1st : _V -onto-> _V
19 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
20 18 19 ax-mp 
 |-  Fun 1st
21 funco 
 |-  ( ( Fun 1st /\ Fun F ) -> Fun ( 1st o. F ) )
22 20 21 mpan 
 |-  ( Fun F -> Fun ( 1st o. F ) )
23 22 adantr 
 |-  ( ( Fun F /\ x e. dom F ) -> Fun ( 1st o. F ) )
24 ssv 
 |-  ( F " dom F ) C_ _V
25 fof 
 |-  ( 1st : _V -onto-> _V -> 1st : _V --> _V )
26 fdm 
 |-  ( 1st : _V --> _V -> dom 1st = _V )
27 18 25 26 mp2b 
 |-  dom 1st = _V
28 24 27 sseqtrri 
 |-  ( F " dom F ) C_ dom 1st
29 ssid 
 |-  dom F C_ dom F
30 funimass3 
 |-  ( ( Fun F /\ dom F C_ dom F ) -> ( ( F " dom F ) C_ dom 1st <-> dom F C_ ( `' F " dom 1st ) ) )
31 29 30 mpan2 
 |-  ( Fun F -> ( ( F " dom F ) C_ dom 1st <-> dom F C_ ( `' F " dom 1st ) ) )
32 28 31 mpbii 
 |-  ( Fun F -> dom F C_ ( `' F " dom 1st ) )
33 32 sselda 
 |-  ( ( Fun F /\ x e. dom F ) -> x e. ( `' F " dom 1st ) )
34 dmco 
 |-  dom ( 1st o. F ) = ( `' F " dom 1st )
35 33 34 eleqtrrdi 
 |-  ( ( Fun F /\ x e. dom F ) -> x e. dom ( 1st o. F ) )
36 fvimacnv 
 |-  ( ( Fun ( 1st o. F ) /\ x e. dom ( 1st o. F ) ) -> ( ( ( 1st o. F ) ` x ) e. Y <-> x e. ( `' ( 1st o. F ) " Y ) ) )
37 23 35 36 syl2anc 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( 1st o. F ) ` x ) e. Y <-> x e. ( `' ( 1st o. F ) " Y ) ) )
38 fo2nd 
 |-  2nd : _V -onto-> _V
39 fofun 
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
40 38 39 ax-mp 
 |-  Fun 2nd
41 funco 
 |-  ( ( Fun 2nd /\ Fun F ) -> Fun ( 2nd o. F ) )
42 40 41 mpan 
 |-  ( Fun F -> Fun ( 2nd o. F ) )
43 42 adantr 
 |-  ( ( Fun F /\ x e. dom F ) -> Fun ( 2nd o. F ) )
44 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
45 fdm 
 |-  ( 2nd : _V --> _V -> dom 2nd = _V )
46 38 44 45 mp2b 
 |-  dom 2nd = _V
47 24 46 sseqtrri 
 |-  ( F " dom F ) C_ dom 2nd
48 funimass3 
 |-  ( ( Fun F /\ dom F C_ dom F ) -> ( ( F " dom F ) C_ dom 2nd <-> dom F C_ ( `' F " dom 2nd ) ) )
49 29 48 mpan2 
 |-  ( Fun F -> ( ( F " dom F ) C_ dom 2nd <-> dom F C_ ( `' F " dom 2nd ) ) )
50 47 49 mpbii 
 |-  ( Fun F -> dom F C_ ( `' F " dom 2nd ) )
51 50 sselda 
 |-  ( ( Fun F /\ x e. dom F ) -> x e. ( `' F " dom 2nd ) )
52 dmco 
 |-  dom ( 2nd o. F ) = ( `' F " dom 2nd )
53 51 52 eleqtrrdi 
 |-  ( ( Fun F /\ x e. dom F ) -> x e. dom ( 2nd o. F ) )
54 fvimacnv 
 |-  ( ( Fun ( 2nd o. F ) /\ x e. dom ( 2nd o. F ) ) -> ( ( ( 2nd o. F ) ` x ) e. Z <-> x e. ( `' ( 2nd o. F ) " Z ) ) )
55 43 53 54 syl2anc 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( 2nd o. F ) ` x ) e. Z <-> x e. ( `' ( 2nd o. F ) " Z ) ) )
56 37 55 anbi12d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) <-> ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) ) )
57 56 adantlr 
 |-  ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( ( ( ( 1st o. F ) ` x ) e. Y /\ ( ( 2nd o. F ) ` x ) e. Z ) <-> ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) ) )
58 15 17 57 3bitr2d 
 |-  ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( ( F ` x ) e. ( Y X. Z ) <-> ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) ) )
59 58 rabbidva 
 |-  ( ( Fun F /\ ran F C_ ( _V X. _V ) ) -> { x e. dom F | ( F ` x ) e. ( Y X. Z ) } = { x e. dom F | ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) } )
60 4 59 eqtrd 
 |-  ( ( Fun F /\ ran F C_ ( _V X. _V ) ) -> ( `' F " ( Y X. Z ) ) = { x e. dom F | ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) } )
61 dfin5 
 |-  ( dom F i^i ( `' ( 1st o. F ) " Y ) ) = { x e. dom F | x e. ( `' ( 1st o. F ) " Y ) }
62 dfin5 
 |-  ( dom F i^i ( `' ( 2nd o. F ) " Z ) ) = { x e. dom F | x e. ( `' ( 2nd o. F ) " Z ) }
63 61 62 ineq12i 
 |-  ( ( dom F i^i ( `' ( 1st o. F ) " Y ) ) i^i ( dom F i^i ( `' ( 2nd o. F ) " Z ) ) ) = ( { x e. dom F | x e. ( `' ( 1st o. F ) " Y ) } i^i { x e. dom F | x e. ( `' ( 2nd o. F ) " Z ) } )
64 cnvimass 
 |-  ( `' ( 1st o. F ) " Y ) C_ dom ( 1st o. F )
65 dmcoss 
 |-  dom ( 1st o. F ) C_ dom F
66 64 65 sstri 
 |-  ( `' ( 1st o. F ) " Y ) C_ dom F
67 sseqin2 
 |-  ( ( `' ( 1st o. F ) " Y ) C_ dom F <-> ( dom F i^i ( `' ( 1st o. F ) " Y ) ) = ( `' ( 1st o. F ) " Y ) )
68 66 67 mpbi 
 |-  ( dom F i^i ( `' ( 1st o. F ) " Y ) ) = ( `' ( 1st o. F ) " Y )
69 cnvimass 
 |-  ( `' ( 2nd o. F ) " Z ) C_ dom ( 2nd o. F )
70 dmcoss 
 |-  dom ( 2nd o. F ) C_ dom F
71 69 70 sstri 
 |-  ( `' ( 2nd o. F ) " Z ) C_ dom F
72 sseqin2 
 |-  ( ( `' ( 2nd o. F ) " Z ) C_ dom F <-> ( dom F i^i ( `' ( 2nd o. F ) " Z ) ) = ( `' ( 2nd o. F ) " Z ) )
73 71 72 mpbi 
 |-  ( dom F i^i ( `' ( 2nd o. F ) " Z ) ) = ( `' ( 2nd o. F ) " Z )
74 68 73 ineq12i 
 |-  ( ( dom F i^i ( `' ( 1st o. F ) " Y ) ) i^i ( dom F i^i ( `' ( 2nd o. F ) " Z ) ) ) = ( ( `' ( 1st o. F ) " Y ) i^i ( `' ( 2nd o. F ) " Z ) )
75 inrab 
 |-  ( { x e. dom F | x e. ( `' ( 1st o. F ) " Y ) } i^i { x e. dom F | x e. ( `' ( 2nd o. F ) " Z ) } ) = { x e. dom F | ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) }
76 63 74 75 3eqtr3ri 
 |-  { x e. dom F | ( x e. ( `' ( 1st o. F ) " Y ) /\ x e. ( `' ( 2nd o. F ) " Z ) ) } = ( ( `' ( 1st o. F ) " Y ) i^i ( `' ( 2nd o. F ) " Z ) )
77 60 76 eqtrdi 
 |-  ( ( Fun F /\ ran F C_ ( _V X. _V ) ) -> ( `' F " ( Y X. Z ) ) = ( ( `' ( 1st o. F ) " Y ) i^i ( `' ( 2nd o. F ) " Z ) ) )