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 \land ran F \subseteq V \times V) \to F^{-1} [Y \times Z] = {(1^{st} \circ F)}^{-1} [Y] \cap {(2^{nd} \circ F)}^{-1} [Z]$

Proof

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

Metamath Proof Explorer

Theorem xppreima

Proof