upxp

Description: Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	upxp.1	$⊢ P = {1^{st} ↾}_{(B \times C)}$
	upxp.2	$⊢ Q = {2^{nd} ↾}_{(B \times C)}$
Assertion	upxp	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to \exists! h (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)$

Proof

Step	Hyp	Ref	Expression
1		upxp.1	$⊢ P = {1^{st} ↾}_{(B \times C)}$
2		upxp.2	$⊢ Q = {2^{nd} ↾}_{(B \times C)}$
3		mptexg	$⊢ A \in D \to (x \in A ⟼ ⟨F (x), G (x)⟩) \in V$
4		eueq	$⊢ (x \in A ⟼ ⟨F (x), G (x)⟩) \in V \leftrightarrow \exists! h h = (x \in A ⟼ ⟨F (x), G (x)⟩)$
5	3 4	sylib	$⊢ A \in D \to \exists! h h = (x \in A ⟼ ⟨F (x), G (x)⟩)$
6	5	3ad2ant1	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to \exists! h h = (x \in A ⟼ ⟨F (x), G (x)⟩)$
7		ffn	$⊢ h : A ⟶ B \times C \to h Fn A$
8	7	3ad2ant1	$⊢ (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \to h Fn A$
9	8	adantl	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \to h Fn A$
10		ffvelrn	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
11		ffvelrn	$⊢ (G : A ⟶ C \land x \in A) \to G (x) \in C$
12		opelxpi	$⊢ (F (x) \in B \land G (x) \in C) \to ⟨F (x), G (x)⟩ \in (B \times C)$
13	10 11 12	syl2an	$⊢ ((F : A ⟶ B \land x \in A) \land (G : A ⟶ C \land x \in A)) \to ⟨F (x), G (x)⟩ \in (B \times C)$
14	13	anandirs	$⊢ ((F : A ⟶ B \land G : A ⟶ C) \land x \in A) \to ⟨F (x), G (x)⟩ \in (B \times C)$
15	14	ralrimiva	$⊢ (F : A ⟶ B \land G : A ⟶ C) \to \forall x \in A ⟨F (x), G (x)⟩ \in (B \times C)$
16	15	3adant1	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to \forall x \in A ⟨F (x), G (x)⟩ \in (B \times C)$
17		eqid	$⊢ (x \in A ⟼ ⟨F (x), G (x)⟩) = (x \in A ⟼ ⟨F (x), G (x)⟩)$
18	17	fmpt	$⊢ \forall x \in A ⟨F (x), G (x)⟩ \in (B \times C) \leftrightarrow (x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C$
19	16 18	sylib	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C$
20	19	ffnd	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (x \in A ⟼ ⟨F (x), G (x)⟩) Fn A$
21	20	adantr	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \to (x \in A ⟼ ⟨F (x), G (x)⟩) Fn A$
22		xpss	$⊢ B \times C \subseteq V \times V$
23		ffvelrn	$⊢ (h : A ⟶ B \times C \land z \in A) \to h (z) \in (B \times C)$
24	22 23	sselid	$⊢ (h : A ⟶ B \times C \land z \in A) \to h (z) \in (V \times V)$
25	24	3ad2antl1	$⊢ ((h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \land z \in A) \to h (z) \in (V \times V)$
26	25	adantll	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to h (z) \in (V \times V)$
27		fveq1	$⊢ F = P \circ h \to F (z) = (P \circ h) (z)$
28	1	coeq1i	$⊢ P \circ h = ({1^{st} ↾}_{(B \times C)}) \circ h$
29	28	fveq1i	$⊢ (P \circ h) (z) = (({1^{st} ↾}_{(B \times C)}) \circ h) (z)$
30	27 29	eqtrdi	$⊢ F = P \circ h \to F (z) = (({1^{st} ↾}_{(B \times C)}) \circ h) (z)$
31	30	3ad2ant2	$⊢ (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \to F (z) = (({1^{st} ↾}_{(B \times C)}) \circ h) (z)$
32	31	ad2antlr	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to F (z) = (({1^{st} ↾}_{(B \times C)}) \circ h) (z)$
33		simpr1	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \to h : A ⟶ B \times C$
34		fvco3	$⊢ (h : A ⟶ B \times C \land z \in A) \to (({1^{st} ↾}_{(B \times C)}) \circ h) (z) = ({1^{st} ↾}_{(B \times C)}) (h (z))$
35	33 34	sylan	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to (({1^{st} ↾}_{(B \times C)}) \circ h) (z) = ({1^{st} ↾}_{(B \times C)}) (h (z))$
36	23	3ad2antl1	$⊢ ((h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \land z \in A) \to h (z) \in (B \times C)$
37	36	adantll	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to h (z) \in (B \times C)$
38	37	fvresd	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to ({1^{st} ↾}_{(B \times C)}) (h (z)) = 1^{st} (h (z))$
39	32 35 38	3eqtrrd	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to 1^{st} (h (z)) = F (z)$
40		fveq1	$⊢ G = Q \circ h \to G (z) = (Q \circ h) (z)$
41	2	coeq1i	$⊢ Q \circ h = ({2^{nd} ↾}_{(B \times C)}) \circ h$
42	41	fveq1i	$⊢ (Q \circ h) (z) = (({2^{nd} ↾}_{(B \times C)}) \circ h) (z)$
43	40 42	eqtrdi	$⊢ G = Q \circ h \to G (z) = (({2^{nd} ↾}_{(B \times C)}) \circ h) (z)$
44	43	3ad2ant3	$⊢ (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \to G (z) = (({2^{nd} ↾}_{(B \times C)}) \circ h) (z)$
45	44	ad2antlr	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to G (z) = (({2^{nd} ↾}_{(B \times C)}) \circ h) (z)$
46		fvco3	$⊢ (h : A ⟶ B \times C \land z \in A) \to (({2^{nd} ↾}_{(B \times C)}) \circ h) (z) = ({2^{nd} ↾}_{(B \times C)}) (h (z))$
47	33 46	sylan	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to (({2^{nd} ↾}_{(B \times C)}) \circ h) (z) = ({2^{nd} ↾}_{(B \times C)}) (h (z))$
48	37	fvresd	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to ({2^{nd} ↾}_{(B \times C)}) (h (z)) = 2^{nd} (h (z))$
49	45 47 48	3eqtrrd	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to 2^{nd} (h (z)) = G (z)$
50		eqopi	$⊢ (h (z) \in (V \times V) \land (1^{st} (h (z)) = F (z) \land 2^{nd} (h (z)) = G (z))) \to h (z) = ⟨F (z), G (z)⟩$
51	26 39 49 50	syl12anc	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to h (z) = ⟨F (z), G (z)⟩$
52		fveq2	$⊢ x = z \to F (x) = F (z)$
53		fveq2	$⊢ x = z \to G (x) = G (z)$
54	52 53	opeq12d	$⊢ x = z \to ⟨F (x), G (x)⟩ = ⟨F (z), G (z)⟩$
55		opex	$⊢ ⟨F (z), G (z)⟩ \in V$
56	54 17 55	fvmpt	$⊢ z \in A \to (x \in A ⟼ ⟨F (x), G (x)⟩) (z) = ⟨F (z), G (z)⟩$
57	56	adantl	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to (x \in A ⟼ ⟨F (x), G (x)⟩) (z) = ⟨F (z), G (z)⟩$
58	51 57	eqtr4d	$⊢ (((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \land z \in A) \to h (z) = (x \in A ⟼ ⟨F (x), G (x)⟩) (z)$
59	9 21 58	eqfnfvd	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)) \to h = (x \in A ⟼ ⟨F (x), G (x)⟩)$
60	59	ex	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to ((h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \to h = (x \in A ⟼ ⟨F (x), G (x)⟩))$
61		ffn	$⊢ F : A ⟶ B \to F Fn A$
62	61	3ad2ant2	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to F Fn A$
63		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
64		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
65	63 64	ax-mp	$⊢ 1^{st} Fn V$
66		ssv	$⊢ B \times C \subseteq V$
67		fnssres	$⊢ (1^{st} Fn V \land B \times C \subseteq V) \to ({1^{st} ↾}_{(B \times C)}) Fn (B \times C)$
68	65 66 67	mp2an	$⊢ ({1^{st} ↾}_{(B \times C)}) Fn (B \times C)$
69	19	frnd	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to ran (x \in A ⟼ ⟨F (x), G (x)⟩) \subseteq B \times C$
70		fnco	$⊢ (({1^{st} ↾}_{(B \times C)}) Fn (B \times C) \land (x \in A ⟼ ⟨F (x), G (x)⟩) Fn A \land ran (x \in A ⟼ ⟨F (x), G (x)⟩) \subseteq B \times C) \to (({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) Fn A$
71	68 20 69 70	mp3an2i	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) Fn A$
72		fvco3	$⊢ ((x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C \land z \in A) \to (({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z) = ({1^{st} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z))$
73	19 72	sylan	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to (({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z) = ({1^{st} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z))$
74	56	adantl	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to (x \in A ⟼ ⟨F (x), G (x)⟩) (z) = ⟨F (z), G (z)⟩$
75	74	fveq2d	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({1^{st} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z)) = ({1^{st} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩)$
76		ffvelrn	$⊢ (F : A ⟶ B \land z \in A) \to F (z) \in B$
77		ffvelrn	$⊢ (G : A ⟶ C \land z \in A) \to G (z) \in C$
78		opelxpi	$⊢ (F (z) \in B \land G (z) \in C) \to ⟨F (z), G (z)⟩ \in (B \times C)$
79	76 77 78	syl2an	$⊢ ((F : A ⟶ B \land z \in A) \land (G : A ⟶ C \land z \in A)) \to ⟨F (z), G (z)⟩ \in (B \times C)$
80	79	anandirs	$⊢ ((F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ⟨F (z), G (z)⟩ \in (B \times C)$
81	80	3adantl1	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ⟨F (z), G (z)⟩ \in (B \times C)$
82	81	fvresd	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({1^{st} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩) = 1^{st} (⟨F (z), G (z)⟩)$
83		fvex	$⊢ F (z) \in V$
84		fvex	$⊢ G (z) \in V$
85	83 84	op1st	$⊢ 1^{st} (⟨F (z), G (z)⟩) = F (z)$
86	82 85	eqtrdi	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({1^{st} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩) = F (z)$
87	73 75 86	3eqtrrd	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to F (z) = (({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z)$
88	62 71 87	eqfnfvd	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to F = ({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
89	1	coeq1i	$⊢ P \circ (x \in A ⟼ ⟨F (x), G (x)⟩) = ({1^{st} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
90	88 89	eqtr4di	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to F = P \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
91		ffn	$⊢ G : A ⟶ C \to G Fn A$
92	91	3ad2ant3	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to G Fn A$
93		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
94		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
95	93 94	ax-mp	$⊢ 2^{nd} Fn V$
96		fnssres	$⊢ (2^{nd} Fn V \land B \times C \subseteq V) \to ({2^{nd} ↾}_{(B \times C)}) Fn (B \times C)$
97	95 66 96	mp2an	$⊢ ({2^{nd} ↾}_{(B \times C)}) Fn (B \times C)$
98		fnco	$⊢ (({2^{nd} ↾}_{(B \times C)}) Fn (B \times C) \land (x \in A ⟼ ⟨F (x), G (x)⟩) Fn A \land ran (x \in A ⟼ ⟨F (x), G (x)⟩) \subseteq B \times C) \to (({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) Fn A$
99	97 20 69 98	mp3an2i	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) Fn A$
100		fvco3	$⊢ ((x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C \land z \in A) \to (({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z) = ({2^{nd} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z))$
101	19 100	sylan	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to (({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z) = ({2^{nd} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z))$
102	74	fveq2d	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({2^{nd} ↾}_{(B \times C)}) ((x \in A ⟼ ⟨F (x), G (x)⟩) (z)) = ({2^{nd} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩)$
103	81	fvresd	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({2^{nd} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩) = 2^{nd} (⟨F (z), G (z)⟩)$
104	83 84	op2nd	$⊢ 2^{nd} (⟨F (z), G (z)⟩) = G (z)$
105	103 104	eqtrdi	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to ({2^{nd} ↾}_{(B \times C)}) (⟨F (z), G (z)⟩) = G (z)$
106	101 102 105	3eqtrrd	$⊢ ((A \in D \land F : A ⟶ B \land G : A ⟶ C) \land z \in A) \to G (z) = (({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)) (z)$
107	92 99 106	eqfnfvd	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to G = ({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
108	2	coeq1i	$⊢ Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩) = ({2^{nd} ↾}_{(B \times C)}) \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
109	107 108	eqtr4di	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to G = Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
110	19 90 109	3jca	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to ((x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C \land F = P \circ (x \in A ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩))$
111		feq1	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to (h : A ⟶ B \times C \leftrightarrow (x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C)$
112		coeq2	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to P \circ h = P \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
113	112	eqeq2d	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to (F = P \circ h \leftrightarrow F = P \circ (x \in A ⟼ ⟨F (x), G (x)⟩))$
114		coeq2	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to Q \circ h = Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩)$
115	114	eqeq2d	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to (G = Q \circ h \leftrightarrow G = Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩))$
116	111 113 115	3anbi123d	$⊢ h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to ((h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \leftrightarrow ((x \in A ⟼ ⟨F (x), G (x)⟩) : A ⟶ B \times C \land F = P \circ (x \in A ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in A ⟼ ⟨F (x), G (x)⟩)))$
117	110 116	syl5ibrcom	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (h = (x \in A ⟼ ⟨F (x), G (x)⟩) \to (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h))$
118	60 117	impbid	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to ((h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \leftrightarrow h = (x \in A ⟼ ⟨F (x), G (x)⟩))$
119	118	eubidv	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to (\exists! h (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h) \leftrightarrow \exists! h h = (x \in A ⟼ ⟨F (x), G (x)⟩))$
120	6 119	mpbird	$⊢ (A \in D \land F : A ⟶ B \land G : A ⟶ C) \to \exists! h (h : A ⟶ B \times C \land F = P \circ h \land G = Q \circ h)$

Metamath Proof Explorer

Theorem upxp

Proof