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 
|- P = ( 1st |` ( B X. C ) )
upxp.2 
|- Q = ( 2nd |` ( B X. C ) )
Assertion upxp 
|- ( ( A e. D /\ F : A --> B /\ G : A --> C ) -> E! h ( h : A --> ( B X. C ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )

Proof

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