fimaproj

Description: Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

	Ref	Expression
Hypotheses	fvproj.h	$⊢ H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$
	fimaproj.f	$⊢ φ \to F Fn A$
	fimaproj.g	$⊢ φ \to G Fn B$
	fimaproj.x	$⊢ φ \to X \subseteq A$
	fimaproj.y	$⊢ φ \to Y \subseteq B$
Assertion	fimaproj	$⊢ φ \to H [X \times Y] = F [X] \times G [Y]$

Proof

Step	Hyp	Ref	Expression
1		fvproj.h	$⊢ H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$
2		fimaproj.f	$⊢ φ \to F Fn A$
3		fimaproj.g	$⊢ φ \to G Fn B$
4		fimaproj.x	$⊢ φ \to X \subseteq A$
5		fimaproj.y	$⊢ φ \to Y \subseteq B$
6		opex	$⊢ ⟨F (1^{st} (z)), G (2^{nd} (z))⟩ \in V$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
10	9	fveq2d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) = F (x)$
11	7 8	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
12	11	fveq2d	$⊢ z = ⟨x, y⟩ \to G (2^{nd} (z)) = G (y)$
13	10 12	opeq12d	$⊢ z = ⟨x, y⟩ \to ⟨F (1^{st} (z)), G (2^{nd} (z))⟩ = ⟨F (x), G (y)⟩$
14	13	mpompt	$⊢ (z \in (A \times B) ⟼ ⟨F (1^{st} (z)), G (2^{nd} (z))⟩) = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$
15	1 14	eqtr4i	$⊢ H = (z \in (A \times B) ⟼ ⟨F (1^{st} (z)), G (2^{nd} (z))⟩)$
16	6 15	fnmpti	$⊢ H Fn (A \times B)$
17		xpss12	$⊢ (X \subseteq A \land Y \subseteq B) \to X \times Y \subseteq A \times B$
18	4 5 17	syl2anc	$⊢ φ \to X \times Y \subseteq A \times B$
19		fvelimab	$⊢ (H Fn (A \times B) \land X \times Y \subseteq A \times B) \to (c \in H [X \times Y] \leftrightarrow \exists z \in (X \times Y) H (z) = c)$
20	16 18 19	sylancr	$⊢ φ \to (c \in H [X \times Y] \leftrightarrow \exists z \in (X \times Y) H (z) = c)$
21		simp-4r	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to a \in X$
22		simplr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to b \in Y$
23		opelxpi	$⊢ (a \in X \land b \in Y) \to ⟨a, b⟩ \in (X \times Y)$
24	21 22 23	syl2anc	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to ⟨a, b⟩ \in (X \times Y)$
25		simpllr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to F (a) = 1^{st} (c)$
26		simpr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to G (b) = 2^{nd} (c)$
27	25 26	opeq12d	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to ⟨F (a), G (b)⟩ = ⟨1^{st} (c), 2^{nd} (c)⟩$
28	4	ad5antr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to X \subseteq A$
29	28 21	sseldd	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to a \in A$
30	5	ad5antr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to Y \subseteq B$
31	30 22	sseldd	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to b \in B$
32	1 29 31	fvproj	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to H (⟨a, b⟩) = ⟨F (a), G (b)⟩$
33		1st2nd2	$⊢ c \in (F [X] \times G [Y]) \to c = ⟨1^{st} (c), 2^{nd} (c)⟩$
34	33	ad5antlr	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to c = ⟨1^{st} (c), 2^{nd} (c)⟩$
35	27 32 34	3eqtr4d	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to H (⟨a, b⟩) = c$
36		fveqeq2	$⊢ z = ⟨a, b⟩ \to (H (z) = c \leftrightarrow H (⟨a, b⟩) = c)$
37	36	rspcev	$⊢ (⟨a, b⟩ \in (X \times Y) \land H (⟨a, b⟩) = c) \to \exists z \in (X \times Y) H (z) = c$
38	24 35 37	syl2anc	$⊢ (((((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \land b \in Y) \land G (b) = 2^{nd} (c)) \to \exists z \in (X \times Y) H (z) = c$
39	3	ad3antrrr	$⊢ (((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \to G Fn B$
40		fnfun	$⊢ G Fn B \to Fun G$
41	39 40	syl	$⊢ (((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \to Fun G$
42		xp2nd	$⊢ c \in (F [X] \times G [Y]) \to 2^{nd} (c) \in G [Y]$
43	42	ad3antlr	$⊢ (((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \to 2^{nd} (c) \in G [Y]$
44		fvelima	$⊢ (Fun G \land 2^{nd} (c) \in G [Y]) \to \exists b \in Y G (b) = 2^{nd} (c)$
45	41 43 44	syl2anc	$⊢ (((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \to \exists b \in Y G (b) = 2^{nd} (c)$
46	38 45	r19.29a	$⊢ (((φ \land c \in (F [X] \times G [Y])) \land a \in X) \land F (a) = 1^{st} (c)) \to \exists z \in (X \times Y) H (z) = c$
47	2	adantr	$⊢ (φ \land c \in (F [X] \times G [Y])) \to F Fn A$
48		fnfun	$⊢ F Fn A \to Fun F$
49	47 48	syl	$⊢ (φ \land c \in (F [X] \times G [Y])) \to Fun F$
50		xp1st	$⊢ c \in (F [X] \times G [Y]) \to 1^{st} (c) \in F [X]$
51	50	adantl	$⊢ (φ \land c \in (F [X] \times G [Y])) \to 1^{st} (c) \in F [X]$
52		fvelima	$⊢ (Fun F \land 1^{st} (c) \in F [X]) \to \exists a \in X F (a) = 1^{st} (c)$
53	49 51 52	syl2anc	$⊢ (φ \land c \in (F [X] \times G [Y])) \to \exists a \in X F (a) = 1^{st} (c)$
54	46 53	r19.29a	$⊢ (φ \land c \in (F [X] \times G [Y])) \to \exists z \in (X \times Y) H (z) = c$
55		simpr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to H (z) = c$
56	18	ad2antrr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to X \times Y \subseteq A \times B$
57		simplr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to z \in (X \times Y)$
58	56 57	sseldd	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to z \in (A \times B)$
59	15	fvmpt2	$⊢ (z \in (A \times B) \land ⟨F (1^{st} (z)), G (2^{nd} (z))⟩ \in V) \to H (z) = ⟨F (1^{st} (z)), G (2^{nd} (z))⟩$
60	58 6 59	sylancl	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to H (z) = ⟨F (1^{st} (z)), G (2^{nd} (z))⟩$
61	2	ad2antrr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to F Fn A$
62	4	ad2antrr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to X \subseteq A$
63		xp1st	$⊢ z \in (X \times Y) \to 1^{st} (z) \in X$
64	57 63	syl	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to 1^{st} (z) \in X$
65		fnfvima	$⊢ (F Fn A \land X \subseteq A \land 1^{st} (z) \in X) \to F (1^{st} (z)) \in F [X]$
66	61 62 64 65	syl3anc	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to F (1^{st} (z)) \in F [X]$
67	3	ad2antrr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to G Fn B$
68	5	ad2antrr	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to Y \subseteq B$
69		xp2nd	$⊢ z \in (X \times Y) \to 2^{nd} (z) \in Y$
70	57 69	syl	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to 2^{nd} (z) \in Y$
71		fnfvima	$⊢ (G Fn B \land Y \subseteq B \land 2^{nd} (z) \in Y) \to G (2^{nd} (z)) \in G [Y]$
72	67 68 70 71	syl3anc	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to G (2^{nd} (z)) \in G [Y]$
73		opelxpi	$⊢ (F (1^{st} (z)) \in F [X] \land G (2^{nd} (z)) \in G [Y]) \to ⟨F (1^{st} (z)), G (2^{nd} (z))⟩ \in (F [X] \times G [Y])$
74	66 72 73	syl2anc	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to ⟨F (1^{st} (z)), G (2^{nd} (z))⟩ \in (F [X] \times G [Y])$
75	60 74	eqeltrd	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to H (z) \in (F [X] \times G [Y])$
76	55 75	eqeltrrd	$⊢ ((φ \land z \in (X \times Y)) \land H (z) = c) \to c \in (F [X] \times G [Y])$
77	76	r19.29an	$⊢ (φ \land \exists z \in (X \times Y) H (z) = c) \to c \in (F [X] \times G [Y])$
78	54 77	impbida	$⊢ φ \to (c \in (F [X] \times G [Y]) \leftrightarrow \exists z \in (X \times Y) H (z) = c)$
79	20 78	bitr4d	$⊢ φ \to (c \in H [X \times Y] \leftrightarrow c \in (F [X] \times G [Y]))$
80	79	eqrdv	$⊢ φ \to H [X \times Y] = F [X] \times G [Y]$

Metamath Proof Explorer

Theorem fimaproj

Proof