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	⊢ 𝑃 = ( 1^st ↾ ( 𝐵 × 𝐶 ) )
	upxp.2	⊢ 𝑄 = ( 2^nd ↾ ( 𝐵 × 𝐶 ) )
Assertion	upxp	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → ∃! ℎ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )

Proof

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

Metamath Proof Explorer

Theorem upxp

Proof