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 ) ) )