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 ) ) )