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	$⊢ φ \to F : A ⟶ B$
	xppreima2.2	$⊢ φ \to G : A ⟶ C$
	xppreima2.3	$⊢ H = (x \in A ⟼ ⟨F (x), G (x)⟩)$
Assertion	xppreima2	$⊢ φ \to H^{-1} [Y \times Z] = F^{-1} [Y] \cap G^{-1} [Z]$

Proof

Step	Hyp	Ref	Expression
1		xppreima2.1	$⊢ φ \to F : A ⟶ B$
2		xppreima2.2	$⊢ φ \to G : A ⟶ C$
3		xppreima2.3	$⊢ H = (x \in A ⟼ ⟨F (x), G (x)⟩)$
4	3	funmpt2	$⊢ Fun H$
5	1	ffvelcdmda	$⊢ (φ \land x \in A) \to F (x) \in B$
6	2	ffvelcdmda	$⊢ (φ \land x \in A) \to G (x) \in C$
7		opelxp	$⊢ ⟨F (x), G (x)⟩ \in (B \times C) \leftrightarrow (F (x) \in B \land G (x) \in C)$
8	5 6 7	sylanbrc	$⊢ (φ \land x \in A) \to ⟨F (x), G (x)⟩ \in (B \times C)$
9	8 3	fmptd	$⊢ φ \to H : A ⟶ B \times C$
10	9	frnd	$⊢ φ \to ran H \subseteq B \times C$
11		xpss	$⊢ B \times C \subseteq V \times V$
12	10 11	sstrdi	$⊢ φ \to ran H \subseteq V \times V$
13		xppreima	$⊢ (Fun H \land ran H \subseteq V \times V) \to H^{-1} [Y \times Z] = {(1^{st} \circ H)}^{-1} [Y] \cap {(2^{nd} \circ H)}^{-1} [Z]$
14	4 12 13	sylancr	$⊢ φ \to H^{-1} [Y \times Z] = {(1^{st} \circ H)}^{-1} [Y] \cap {(2^{nd} \circ H)}^{-1} [Z]$
15		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
16		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
17	15 16	ax-mp	$⊢ 1^{st} Fn V$
18		opex	$⊢ ⟨F (x), G (x)⟩ \in V$
19	18 3	fnmpti	$⊢ H Fn A$
20		ssv	$⊢ ran H \subseteq V$
21		fnco	$⊢ (1^{st} Fn V \land H Fn A \land ran H \subseteq V) \to (1^{st} \circ H) Fn A$
22	17 19 20 21	mp3an	$⊢ (1^{st} \circ H) Fn A$
23	22	a1i	$⊢ φ \to (1^{st} \circ H) Fn A$
24	1	ffnd	$⊢ φ \to F Fn A$
25	4	a1i	$⊢ (φ \land x \in A) \to Fun H$
26	12	adantr	$⊢ (φ \land x \in A) \to ran H \subseteq V \times V$
27		simpr	$⊢ (φ \land x \in A) \to x \in A$
28	18 3	dmmpti	$⊢ dom H = A$
29	27 28	eleqtrrdi	$⊢ (φ \land x \in A) \to x \in dom H$
30		opfv	$⊢ ((Fun H \land ran H \subseteq V \times V) \land x \in dom H) \to H (x) = ⟨(1^{st} \circ H) (x), (2^{nd} \circ H) (x)⟩$
31	25 26 29 30	syl21anc	$⊢ (φ \land x \in A) \to H (x) = ⟨(1^{st} \circ H) (x), (2^{nd} \circ H) (x)⟩$
32	3	fvmpt2	$⊢ (x \in A \land ⟨F (x), G (x)⟩ \in (B \times C)) \to H (x) = ⟨F (x), G (x)⟩$
33	27 8 32	syl2anc	$⊢ (φ \land x \in A) \to H (x) = ⟨F (x), G (x)⟩$
34	31 33	eqtr3d	$⊢ (φ \land x \in A) \to ⟨(1^{st} \circ H) (x), (2^{nd} \circ H) (x)⟩ = ⟨F (x), G (x)⟩$
35		fvex	$⊢ (1^{st} \circ H) (x) \in V$
36		fvex	$⊢ (2^{nd} \circ H) (x) \in V$
37	35 36	opth	$⊢ ⟨(1^{st} \circ H) (x), (2^{nd} \circ H) (x)⟩ = ⟨F (x), G (x)⟩ \leftrightarrow ((1^{st} \circ H) (x) = F (x) \land (2^{nd} \circ H) (x) = G (x))$
38	34 37	sylib	$⊢ (φ \land x \in A) \to ((1^{st} \circ H) (x) = F (x) \land (2^{nd} \circ H) (x) = G (x))$
39	38	simpld	$⊢ (φ \land x \in A) \to (1^{st} \circ H) (x) = F (x)$
40	23 24 39	eqfnfvd	$⊢ φ \to 1^{st} \circ H = F$
41	40	cnveqd	$⊢ φ \to {(1^{st} \circ H)}^{-1} = F^{-1}$
42	41	imaeq1d	$⊢ φ \to {(1^{st} \circ H)}^{-1} [Y] = F^{-1} [Y]$
43		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
44		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
45	43 44	ax-mp	$⊢ 2^{nd} Fn V$
46		fnco	$⊢ (2^{nd} Fn V \land H Fn A \land ran H \subseteq V) \to (2^{nd} \circ H) Fn A$
47	45 19 20 46	mp3an	$⊢ (2^{nd} \circ H) Fn A$
48	47	a1i	$⊢ φ \to (2^{nd} \circ H) Fn A$
49	2	ffnd	$⊢ φ \to G Fn A$
50	38	simprd	$⊢ (φ \land x \in A) \to (2^{nd} \circ H) (x) = G (x)$
51	48 49 50	eqfnfvd	$⊢ φ \to 2^{nd} \circ H = G$
52	51	cnveqd	$⊢ φ \to {(2^{nd} \circ H)}^{-1} = G^{-1}$
53	52	imaeq1d	$⊢ φ \to {(2^{nd} \circ H)}^{-1} [Z] = G^{-1} [Z]$
54	42 53	ineq12d	$⊢ φ \to {(1^{st} \circ H)}^{-1} [Y] \cap {(2^{nd} \circ H)}^{-1} [Z] = F^{-1} [Y] \cap G^{-1} [Z]$
55	14 54	eqtrd	$⊢ φ \to H^{-1} [Y \times Z] = F^{-1} [Y] \cap G^{-1} [Z]$

Metamath Proof Explorer

Theorem xppreima2

Proof