Metamath Proof Explorer

Theorem uptx

Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses uptx.1 
|- T = ( R tX S )
uptx.2 
|- X = U. R
uptx.3 
|- Y = U. S
uptx.4 
|- Z = ( X X. Y )
uptx.5 
|- P = ( 1st |` Z )
uptx.6 
|- Q = ( 2nd |` Z )
Assertion uptx 
|- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) )

Proof

Step Hyp Ref Expression
1 uptx.1 
 |-  T = ( R tX S )
2 uptx.2 
 |-  X = U. R
3 uptx.3 
 |-  Y = U. S
4 uptx.4 
 |-  Z = ( X X. Y )
5 uptx.5 
 |-  P = ( 1st |` Z )
6 uptx.6 
 |-  Q = ( 2nd |` Z )
7 eqid 
 |-  U. U = U. U
8 eqid 
 |-  ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. )
9 7 8 txcnmpt 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn ( R tX S ) ) )
10 1 oveq2i 
 |-  ( U Cn T ) = ( U Cn ( R tX S ) )
11 9 10 eleqtrrdi 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) )
12 7 2 cnf 
 |-  ( F e. ( U Cn R ) -> F : U. U --> X )
13 7 3 cnf 
 |-  ( G e. ( U Cn S ) -> G : U. U --> Y )
14 ffn 
 |-  ( F : U. U --> X -> F Fn U. U )
15 14 adantr 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> F Fn U. U )
16 fo1st 
 |-  1st : _V -onto-> _V
17 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
18 16 17 ax-mp 
 |-  1st Fn _V
19 ssv 
 |-  ( X X. Y ) C_ _V
20 fnssres 
 |-  ( ( 1st Fn _V /\ ( X X. Y ) C_ _V ) -> ( 1st |` ( X X. Y ) ) Fn ( X X. Y ) )
21 18 19 20 mp2an 
 |-  ( 1st |` ( X X. Y ) ) Fn ( X X. Y )
22 ffvelrn 
 |-  ( ( F : U. U --> X /\ x e. U. U ) -> ( F ` x ) e. X )
23 ffvelrn 
 |-  ( ( G : U. U --> Y /\ x e. U. U ) -> ( G ` x ) e. Y )
24 opelxpi 
 |-  ( ( ( F ` x ) e. X /\ ( G ` x ) e. Y ) -> <. ( F ` x ) , ( G ` x ) >. e. ( X X. Y ) )
25 22 23 24 syl2an 
 |-  ( ( ( F : U. U --> X /\ x e. U. U ) /\ ( G : U. U --> Y /\ x e. U. U ) ) -> <. ( F ` x ) , ( G ` x ) >. e. ( X X. Y ) )
26 25 anandirs 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ x e. U. U ) -> <. ( F ` x ) , ( G ` x ) >. e. ( X X. Y ) )
27 26 fmpttd 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) : U. U --> ( X X. Y ) )
28 ffn 
 |-  ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) : U. U --> ( X X. Y ) -> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) Fn U. U )
29 27 28 syl 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) Fn U. U )
30 27 frnd 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> ran ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) C_ ( X X. Y ) )
31 fnco 
 |-  ( ( ( 1st |` ( X X. Y ) ) Fn ( X X. Y ) /\ ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) Fn U. U /\ ran ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) C_ ( X X. Y ) ) -> ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) Fn U. U )
32 21 29 30 31 mp3an2i 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) Fn U. U )
33 fvco3 
 |-  ( ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) : U. U --> ( X X. Y ) /\ z e. U. U ) -> ( ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) = ( ( 1st |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) )
34 27 33 sylan 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) = ( ( 1st |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) )
35 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
36 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
37 35 36 opeq12d 
 |-  ( x = z -> <. ( F ` x ) , ( G ` x ) >. = <. ( F ` z ) , ( G ` z ) >. )
38 opex 
 |-  <. ( F ` z ) , ( G ` z ) >. e. _V
39 37 8 38 fvmpt 
 |-  ( z e. U. U -> ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) = <. ( F ` z ) , ( G ` z ) >. )
40 39 adantl 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) = <. ( F ` z ) , ( G ` z ) >. )
41 40 fveq2d 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 1st |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) = ( ( 1st |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) )
42 ffvelrn 
 |-  ( ( F : U. U --> X /\ z e. U. U ) -> ( F ` z ) e. X )
43 ffvelrn 
 |-  ( ( G : U. U --> Y /\ z e. U. U ) -> ( G ` z ) e. Y )
44 opelxpi 
 |-  ( ( ( F ` z ) e. X /\ ( G ` z ) e. Y ) -> <. ( F ` z ) , ( G ` z ) >. e. ( X X. Y ) )
45 42 43 44 syl2an 
 |-  ( ( ( F : U. U --> X /\ z e. U. U ) /\ ( G : U. U --> Y /\ z e. U. U ) ) -> <. ( F ` z ) , ( G ` z ) >. e. ( X X. Y ) )
46 45 anandirs 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> <. ( F ` z ) , ( G ` z ) >. e. ( X X. Y ) )
47 46 fvresd 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 1st |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) = ( 1st ` <. ( F ` z ) , ( G ` z ) >. ) )
48 fvex 
 |-  ( F ` z ) e. _V
49 fvex 
 |-  ( G ` z ) e. _V
50 48 49 op1st 
 |-  ( 1st ` <. ( F ` z ) , ( G ` z ) >. ) = ( F ` z )
51 47 50 eqtrdi 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 1st |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) = ( F ` z ) )
52 34 41 51 3eqtrrd 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( F ` z ) = ( ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) )
53 15 32 52 eqfnfvd 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> F = ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
54 4 reseq2i 
 |-  ( 1st |` Z ) = ( 1st |` ( X X. Y ) )
55 5 54 eqtri 
 |-  P = ( 1st |` ( X X. Y ) )
56 55 coeq1i 
 |-  ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) = ( ( 1st |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) )
57 53 56 eqtr4di 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
58 12 13 57 syl2an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
59 ffn 
 |-  ( G : U. U --> Y -> G Fn U. U )
60 59 adantl 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> G Fn U. U )
61 fo2nd 
 |-  2nd : _V -onto-> _V
62 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
63 61 62 ax-mp 
 |-  2nd Fn _V
64 fnssres 
 |-  ( ( 2nd Fn _V /\ ( X X. Y ) C_ _V ) -> ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) )
65 63 19 64 mp2an 
 |-  ( 2nd |` ( X X. Y ) ) Fn ( X X. Y )
66 fnco 
 |-  ( ( ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) /\ ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) Fn U. U /\ ran ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) C_ ( X X. Y ) ) -> ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) Fn U. U )
67 65 29 30 66 mp3an2i 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) Fn U. U )
68 fvco3 
 |-  ( ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) : U. U --> ( X X. Y ) /\ z e. U. U ) -> ( ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) = ( ( 2nd |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) )
69 27 68 sylan 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) = ( ( 2nd |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) )
70 40 fveq2d 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 2nd |` ( X X. Y ) ) ` ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ` z ) ) = ( ( 2nd |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) )
71 46 fvresd 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 2nd |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) = ( 2nd ` <. ( F ` z ) , ( G ` z ) >. ) )
72 48 49 op2nd 
 |-  ( 2nd ` <. ( F ` z ) , ( G ` z ) >. ) = ( G ` z )
73 71 72 eqtrdi 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( ( 2nd |` ( X X. Y ) ) ` <. ( F ` z ) , ( G ` z ) >. ) = ( G ` z ) )
74 69 70 73 3eqtrrd 
 |-  ( ( ( F : U. U --> X /\ G : U. U --> Y ) /\ z e. U. U ) -> ( G ` z ) = ( ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ` z ) )
75 60 67 74 eqfnfvd 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> G = ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
76 4 reseq2i 
 |-  ( 2nd |` Z ) = ( 2nd |` ( X X. Y ) )
77 6 76 eqtri 
 |-  Q = ( 2nd |` ( X X. Y ) )
78 77 coeq1i 
 |-  ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) = ( ( 2nd |` ( X X. Y ) ) o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) )
79 75 78 eqtr4di 
 |-  ( ( F : U. U --> X /\ G : U. U --> Y ) -> G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
80 12 13 79 syl2an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
81 11 58 80 jca32 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) /\ ( F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) /\ G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) ) )
82 eleq1 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( h e. ( U Cn T ) <-> ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) ) )
83 coeq2 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( P o. h ) = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
84 83 eqeq2d 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( F = ( P o. h ) <-> F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) )
85 coeq2 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( Q o. h ) = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) )
86 85 eqeq2d 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( G = ( Q o. h ) <-> G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) )
87 84 86 anbi12d 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( ( F = ( P o. h ) /\ G = ( Q o. h ) ) <-> ( F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) /\ G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) ) )
88 82 87 anbi12d 
 |-  ( h = ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) -> ( ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) <-> ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) /\ ( F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) /\ G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) ) ) )
89 88 spcegv 
 |-  ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) -> ( ( ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) e. ( U Cn T ) /\ ( F = ( P o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) /\ G = ( Q o. ( x e. U. U |-> <. ( F ` x ) , ( G ` x ) >. ) ) ) ) -> E. h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) ) )
90 11 81 89 sylc 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E. h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
91 eqid 
 |-  U. T = U. T
92 7 91 cnf 
 |-  ( h e. ( U Cn T ) -> h : U. U --> U. T )
93 cntop2 
 |-  ( F e. ( U Cn R ) -> R e. Top )
94 cntop2 
 |-  ( G e. ( U Cn S ) -> S e. Top )
95 1 unieqi 
 |-  U. T = U. ( R tX S )
96 2 3 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
97 95 96 eqtr4id 
 |-  ( ( R e. Top /\ S e. Top ) -> U. T = ( X X. Y ) )
98 93 94 97 syl2an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> U. T = ( X X. Y ) )
99 98 feq3d 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( h : U. U --> U. T <-> h : U. U --> ( X X. Y ) ) )
100 92 99 syl5ib 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( h e. ( U Cn T ) -> h : U. U --> ( X X. Y ) ) )
101 100 anim1d 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) -> ( h : U. U --> ( X X. Y ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) ) )
102 3anass 
 |-  ( ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) <-> ( h : U. U --> ( X X. Y ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
103 101 102 syl6ibr 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) -> ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
104 103 alrimiv 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> A. h ( ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) -> ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
105 cntop1 
 |-  ( F e. ( U Cn R ) -> U e. Top )
106 105 uniexd 
 |-  ( F e. ( U Cn R ) -> U. U e. _V )
107 55 77 upxp 
 |-  ( ( U. U e. _V /\ F : U. U --> X /\ G : U. U --> Y ) -> E! h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
108 106 12 13 107 syl2an3an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
109 eumo 
 |-  ( E! h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) -> E* h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
110 108 109 syl 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E* h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
111 moim 
 |-  ( A. h ( ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) -> ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) ) -> ( E* h ( h : U. U --> ( X X. Y ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) -> E* h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) ) )
112 104 110 111 sylc 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E* h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
113 df-reu 
 |-  ( E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) <-> E! h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) )
114 df-eu 
 |-  ( E! h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) <-> ( E. h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) /\ E* h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) ) )
115 113 114 bitri 
 |-  ( E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) <-> ( E. h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) /\ E* h ( h e. ( U Cn T ) /\ ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) ) )
116 90 112 115 sylanbrc 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) )