This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 upxp.1 ⊢ 𝑃 = ( 1st ↾ ( 𝐵 × 𝐶 ) )
2 upxp.2 ⊢ 𝑄 = ( 2nd ↾ ( 𝐵 × 𝐶 ) )
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 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11 ffvelcdm ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
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 ffvelcdm ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( 𝐵 × 𝐶 ) )
24 22 23 sselid ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( V × V ) )
25 24 3ad2antl1 ⊢ ( ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( V × V ) )
26 25 adantll ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( V × V ) )
27 fveq1 ⊢ ( 𝐹 = ( 𝑃 ∘ ℎ ) → ( 𝐹 ‘ 𝑧 ) = ( ( 𝑃 ∘ ℎ ) ‘ 𝑧 ) )
28 1 coeq1i ⊢ ( 𝑃 ∘ ℎ ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ )
29 28 fveq1i ⊢ ( ( 𝑃 ∘ ℎ ) ‘ 𝑧 ) = ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 )
30 27 29 eqtrdi ⊢ ( 𝐹 = ( 𝑃 ∘ ℎ ) → ( 𝐹 ‘ 𝑧 ) = ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
31 30 3ad2ant2 ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) → ( 𝐹 ‘ 𝑧 ) = ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
32 31 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
33 simpr1 ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) )
34 fvco3 ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) )
35 33 34 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) )
36 23 3ad2antl1 ⊢ ( ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( 𝐵 × 𝐶 ) )
37 36 adantll ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ℎ ‘ 𝑧 ) ∈ ( 𝐵 × 𝐶 ) )
38 37 fvresd ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) = ( 1st ‘ ( ℎ ‘ 𝑧 ) ) )
39 32 35 38 3eqtrrd ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 1st ‘ ( ℎ ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
40 fveq1 ⊢ ( 𝐺 = ( 𝑄 ∘ ℎ ) → ( 𝐺 ‘ 𝑧 ) = ( ( 𝑄 ∘ ℎ ) ‘ 𝑧 ) )
41 2 coeq1i ⊢ ( 𝑄 ∘ ℎ ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ )
42 41 fveq1i ⊢ ( ( 𝑄 ∘ ℎ ) ‘ 𝑧 ) = ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 )
43 40 42 eqtrdi ⊢ ( 𝐺 = ( 𝑄 ∘ ℎ ) → ( 𝐺 ‘ 𝑧 ) = ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
44 43 3ad2ant3 ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) → ( 𝐺 ‘ 𝑧 ) = ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
45 44 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) = ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) )
46 fvco3 ⊢ ( ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) )
47 33 46 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ℎ ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) )
48 37 fvresd ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ℎ ‘ 𝑧 ) ) = ( 2nd ‘ ( ℎ ‘ 𝑧 ) ) )
49 45 47 48 3eqtrrd ⊢ ( ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 2nd ‘ ( ℎ ‘ 𝑧 ) ) = ( 𝐺 ‘ 𝑧 ) )
50 eqopi ⊢ ( ( ( ℎ ‘ 𝑧 ) ∈ ( V × V ) ∧ ( ( 1st ‘ ( ℎ ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) ∧ ( 2nd ‘ ( ℎ ‘ 𝑧 ) ) = ( 𝐺 ‘ 𝑧 ) ) ) → ( ℎ ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ )
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 ⊢ 1st : V –onto→ V
64 fofn ⊢ ( 1st : V –onto→ V → 1st Fn V )
65 63 64 ax-mp ⊢ 1st Fn V
66 ssv ⊢ ( 𝐵 × 𝐶 ) ⊆ V
67 fnssres ⊢ ( ( 1st Fn V ∧ ( 𝐵 × 𝐶 ) ⊆ V ) → ( 1st ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 ) )
68 65 66 67 mp2an ⊢ ( 1st ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 )
69 19 frnd ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → ran ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝐵 × 𝐶 ) )
70 fnco ⊢ ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝐵 × 𝐶 ) ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn 𝐴 )
71 68 20 69 70 mp3an2i ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn 𝐴 )
72 fvco3 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
73 19 72 sylan ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
74 56 adantl ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ )
75 74 fveq2d ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
76 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
77 ffvelcdm ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐶 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐶 )
78 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑧 ) ∈ 𝐶 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
79 76 77 78 syl2an ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐶 ∧ 𝑧 ∈ 𝐴 ) ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
80 79 anandirs ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
81 80 3adantl1 ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
82 81 fvresd ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 1st ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
83 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
84 fvex ⊢ ( 𝐺 ‘ 𝑧 ) ∈ V
85 83 84 op1st ⊢ ( 1st ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐹 ‘ 𝑧 )
86 82 85 eqtrdi ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐹 ‘ 𝑧 ) )
87 73 75 86 3eqtrrd ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
88 62 71 87 eqfnfvd ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → 𝐹 = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
89 1 coeq1i ⊢ ( 𝑃 ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) = ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
90 88 89 eqtr4di ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
91 ffn ⊢ ( 𝐺 : 𝐴 ⟶ 𝐶 → 𝐺 Fn 𝐴 )
92 91 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → 𝐺 Fn 𝐴 )
93 fo2nd ⊢ 2nd : V –onto→ V
94 fofn ⊢ ( 2nd : V –onto→ V → 2nd Fn V )
95 93 94 ax-mp ⊢ 2nd Fn V
96 fnssres ⊢ ( ( 2nd Fn V ∧ ( 𝐵 × 𝐶 ) ⊆ V ) → ( 2nd ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 ) )
97 95 66 96 mp2an ⊢ ( 2nd ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 )
98 fnco ⊢ ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) Fn ( 𝐵 × 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝐵 × 𝐶 ) ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn 𝐴 )
99 97 20 69 98 mp3an2i ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn 𝐴 )
100 fvco3 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
101 19 100 sylan ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
102 74 fveq2d ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
103 81 fvresd ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 2nd ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
104 83 84 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐺 ‘ 𝑧 )
105 103 104 eqtrdi ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐺 ‘ 𝑧 ) )
106 101 102 105 3eqtrrd ⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) = ( ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
107 92 99 106 eqfnfvd ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → 𝐺 = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
108 2 coeq1i ⊢ ( 𝑄 ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) = ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
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 ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐴 ⟶ 𝐶 ) → ∃! ℎ ( ℎ : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )