Metamath Proof Explorer

Theorem txlm

Description: Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of Gleason p. 230. (Contributed by NM, 16-Jul-2007) (Revised by Mario Carneiro, 5-May-2014)

Ref Expression
Hypotheses txlm.z 
|- Z = ( ZZ>= ` M )
txlm.m 
|- ( ph -> M e. ZZ )
txlm.j 
|- ( ph -> J e. ( TopOn ` X ) )
txlm.k 
|- ( ph -> K e. ( TopOn ` Y ) )
txlm.f 
|- ( ph -> F : Z --> X )
txlm.g 
|- ( ph -> G : Z --> Y )
txlm.h 
|- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )
Assertion txlm 
|- ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> H ( ~~>t ` ( J tX K ) ) <. R , S >. ) )

Proof

Step Hyp Ref Expression
1 txlm.z 
 |-  Z = ( ZZ>= ` M )
2 txlm.m 
 |-  ( ph -> M e. ZZ )
3 txlm.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 txlm.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
5 txlm.f 
 |-  ( ph -> F : Z --> X )
6 txlm.g 
 |-  ( ph -> G : Z --> Y )
7 txlm.h 
 |-  H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )
8 r19.27v 
 |-  ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
9 r19.28v 
 |-  ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
10 9 ralimi 
 |-  ( A. u e. J ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
11 8 10 syl 
 |-  ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
12 simprl 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> w e. ( J tX K ) )
13 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
14 3 13 syl 
 |-  ( ph -> J e. Top )
15 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
16 4 15 syl 
 |-  ( ph -> K e. Top )
17 eqid 
 |-  ran ( u e. J , v e. K |-> ( u X. v ) ) = ran ( u e. J , v e. K |-> ( u X. v ) )
18 17 txval 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
19 14 16 18 syl2anc 
 |-  ( ph -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
20 19 adantr 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
21 12 20 eleqtrd 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> w e. ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
22 simprr 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> <. R , S >. e. w )
23 tg2 
 |-  ( ( w e. ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) /\ <. R , S >. e. w ) -> E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) )
24 21 22 23 syl2anc 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) )
25 vex 
 |-  u e. _V
26 vex 
 |-  v e. _V
27 25 26 xpex 
 |-  ( u X. v ) e. _V
28 27 rgen2w 
 |-  A. u e. J A. v e. K ( u X. v ) e. _V
29 eqid 
 |-  ( u e. J , v e. K |-> ( u X. v ) ) = ( u e. J , v e. K |-> ( u X. v ) )
30 eleq2 
 |-  ( t = ( u X. v ) -> ( <. R , S >. e. t <-> <. R , S >. e. ( u X. v ) ) )
31 sseq1 
 |-  ( t = ( u X. v ) -> ( t C_ w <-> ( u X. v ) C_ w ) )
32 30 31 anbi12d 
 |-  ( t = ( u X. v ) -> ( ( <. R , S >. e. t /\ t C_ w ) <-> ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
33 29 32 rexrnmpo 
 |-  ( A. u e. J A. v e. K ( u X. v ) e. _V -> ( E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) <-> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
34 28 33 ax-mp 
 |-  ( E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) <-> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) )
35 24 34 sylib 
 |-  ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) )
36 35 ex 
 |-  ( ph -> ( ( w e. ( J tX K ) /\ <. R , S >. e. w ) -> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
37 r19.29 
 |-  ( ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. u e. J ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
38 r19.29 
 |-  ( ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. v e. K ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) )
39 simprl 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> <. R , S >. e. ( u X. v ) )
40 opelxp 
 |-  ( <. R , S >. e. ( u X. v ) <-> ( R e. u /\ S e. v ) )
41 39 40 sylib 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( R e. u /\ S e. v ) )
42 pm2.27 
 |-  ( R e. u -> ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
43 pm2.27 
 |-  ( S e. v -> ( ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) )
44 42 43 im2anan9 
 |-  ( ( R e. u /\ S e. v ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
45 41 44 syl 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
46 1 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) )
47 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
48 opelxpi 
 |-  ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> <. ( F ` k ) , ( G ` k ) >. e. ( u X. v ) )
49 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
50 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
51 49 50 opeq12d 
 |-  ( n = k -> <. ( F ` n ) , ( G ` n ) >. = <. ( F ` k ) , ( G ` k ) >. )
52 opex 
 |-  <. ( F ` k ) , ( G ` k ) >. e. _V
53 51 7 52 fvmpt 
 |-  ( k e. Z -> ( H ` k ) = <. ( F ` k ) , ( G ` k ) >. )
54 53 eleq1d 
 |-  ( k e. Z -> ( ( H ` k ) e. ( u X. v ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( u X. v ) ) )
55 48 54 imbitrrid 
 |-  ( k e. Z -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. ( u X. v ) ) )
56 55 adantl 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. ( u X. v ) ) )
57 simplrr 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( u X. v ) C_ w )
58 57 sseld 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( H ` k ) e. ( u X. v ) -> ( H ` k ) e. w ) )
59 56 58 syld 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) )
60 47 59 sylan2 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) )
61 60 anassrs 
 |-  ( ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) )
62 61 ralimdva 
 |-  ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
63 62 reximdva 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
64 46 63 biimtrrid 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
65 45 64 syld 
 |-  ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
66 65 ex 
 |-  ( ( ( ph /\ u e. J ) /\ v e. K ) -> ( ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
67 66 impcomd 
 |-  ( ( ( ph /\ u e. J ) /\ v e. K ) -> ( ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
68 67 rexlimdva 
 |-  ( ( ph /\ u e. J ) -> ( E. v e. K ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
69 38 68 syl5 
 |-  ( ( ph /\ u e. J ) -> ( ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
70 69 rexlimdva 
 |-  ( ph -> ( E. u e. J ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
71 37 70 syl5 
 |-  ( ph -> ( ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) )
72 71 expcomd 
 |-  ( ph -> ( E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
73 36 72 syld 
 |-  ( ph -> ( ( w e. ( J tX K ) /\ <. R , S >. e. w ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
74 73 expdimp 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( <. R , S >. e. w -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
75 74 com23 
 |-  ( ( ph /\ w e. ( J tX K ) ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
76 75 ralrimdva 
 |-  ( ph -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
77 11 76 syl5 
 |-  ( ph -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
78 77 adantr 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
79 14 adantr 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> J e. Top )
80 16 adantr 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> K e. Top )
81 simprr 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> u e. J )
82 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
83 4 82 syl 
 |-  ( ph -> Y e. K )
84 83 adantr 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> Y e. K )
85 txopn 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( u e. J /\ Y e. K ) ) -> ( u X. Y ) e. ( J tX K ) )
86 79 80 81 84 85 syl22anc 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( u X. Y ) e. ( J tX K ) )
87 eleq2 
 |-  ( w = ( u X. Y ) -> ( <. R , S >. e. w <-> <. R , S >. e. ( u X. Y ) ) )
88 eleq2 
 |-  ( w = ( u X. Y ) -> ( ( H ` k ) e. w <-> ( H ` k ) e. ( u X. Y ) ) )
89 88 rexralbidv 
 |-  ( w = ( u X. Y ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) )
90 87 89 imbi12d 
 |-  ( w = ( u X. Y ) -> ( ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) <-> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) )
91 90 rspcv 
 |-  ( ( u X. Y ) e. ( J tX K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) )
92 86 91 syl 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) )
93 simprl 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> S e. Y )
94 opelxpi 
 |-  ( ( R e. u /\ S e. Y ) -> <. R , S >. e. ( u X. Y ) )
95 93 94 sylan2 
 |-  ( ( R e. u /\ ( ph /\ ( S e. Y /\ u e. J ) ) ) -> <. R , S >. e. ( u X. Y ) )
96 95 expcom 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( R e. u -> <. R , S >. e. ( u X. Y ) ) )
97 53 eleq1d 
 |-  ( k e. Z -> ( ( H ` k ) e. ( u X. Y ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( u X. Y ) ) )
98 opelxp1 
 |-  ( <. ( F ` k ) , ( G ` k ) >. e. ( u X. Y ) -> ( F ` k ) e. u )
99 97 98 biimtrdi 
 |-  ( k e. Z -> ( ( H ` k ) e. ( u X. Y ) -> ( F ` k ) e. u ) )
100 47 99 syl 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( H ` k ) e. ( u X. Y ) -> ( F ` k ) e. u ) )
101 100 ralimdva 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
102 101 reximia 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u )
103 102 a1i 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
104 96 103 imim12d 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
105 92 104 syld 
 |-  ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
106 105 anassrs 
 |-  ( ( ( ph /\ S e. Y ) /\ u e. J ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
107 106 ralrimdva 
 |-  ( ( ph /\ S e. Y ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
108 107 adantrl 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) )
109 14 adantr 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> J e. Top )
110 16 adantr 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> K e. Top )
111 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
112 3 111 syl 
 |-  ( ph -> X e. J )
113 112 adantr 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> X e. J )
114 simprr 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> v e. K )
115 txopn 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( X e. J /\ v e. K ) ) -> ( X X. v ) e. ( J tX K ) )
116 109 110 113 114 115 syl22anc 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( X X. v ) e. ( J tX K ) )
117 eleq2 
 |-  ( w = ( X X. v ) -> ( <. R , S >. e. w <-> <. R , S >. e. ( X X. v ) ) )
118 eleq2 
 |-  ( w = ( X X. v ) -> ( ( H ` k ) e. w <-> ( H ` k ) e. ( X X. v ) ) )
119 118 rexralbidv 
 |-  ( w = ( X X. v ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) )
120 117 119 imbi12d 
 |-  ( w = ( X X. v ) -> ( ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) <-> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) )
121 120 rspcv 
 |-  ( ( X X. v ) e. ( J tX K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) )
122 116 121 syl 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) )
123 opelxpi 
 |-  ( ( R e. X /\ S e. v ) -> <. R , S >. e. ( X X. v ) )
124 123 ex 
 |-  ( R e. X -> ( S e. v -> <. R , S >. e. ( X X. v ) ) )
125 124 ad2antrl 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( S e. v -> <. R , S >. e. ( X X. v ) ) )
126 53 eleq1d 
 |-  ( k e. Z -> ( ( H ` k ) e. ( X X. v ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( X X. v ) ) )
127 opelxp2 
 |-  ( <. ( F ` k ) , ( G ` k ) >. e. ( X X. v ) -> ( G ` k ) e. v )
128 126 127 biimtrdi 
 |-  ( k e. Z -> ( ( H ` k ) e. ( X X. v ) -> ( G ` k ) e. v ) )
129 47 128 syl 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( H ` k ) e. ( X X. v ) -> ( G ` k ) e. v ) )
130 129 ralimdva 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) )
131 130 reximia 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v )
132 131 a1i 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) )
133 125 132 imim12d 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
134 122 133 syld 
 |-  ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
135 134 anassrs 
 |-  ( ( ( ph /\ R e. X ) /\ v e. K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
136 135 ralrimdva 
 |-  ( ( ph /\ R e. X ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
137 136 adantrr 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) )
138 108 137 jcad 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) )
139 78 138 impbid 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) <-> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
140 139 pm5.32da 
 |-  ( ph -> ( ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( ( R e. X /\ S e. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) )
141 opelxp 
 |-  ( <. R , S >. e. ( X X. Y ) <-> ( R e. X /\ S e. Y ) )
142 141 anbi1i 
 |-  ( ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) <-> ( ( R e. X /\ S e. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) )
143 140 142 bitr4di 
 |-  ( ph -> ( ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) )
144 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
145 3 1 2 5 144 lmbrf 
 |-  ( ph -> ( F ( ~~>t ` J ) R <-> ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) )
146 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
147 4 1 2 6 146 lmbrf 
 |-  ( ph -> ( G ( ~~>t ` K ) S <-> ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) )
148 145 147 anbi12d 
 |-  ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) )
149 an4 
 |-  ( ( ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) )
150 148 149 bitrdi 
 |-  ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) )
151 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
152 3 4 151 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
153 5 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
154 6 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) e. Y )
155 153 154 opelxpd 
 |-  ( ( ph /\ n e. Z ) -> <. ( F ` n ) , ( G ` n ) >. e. ( X X. Y ) )
156 155 7 fmptd 
 |-  ( ph -> H : Z --> ( X X. Y ) )
157 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( H ` k ) )
158 152 1 2 156 157 lmbrf 
 |-  ( ph -> ( H ( ~~>t ` ( J tX K ) ) <. R , S >. <-> ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) )
159 143 150 158 3bitr4d 
 |-  ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> H ( ~~>t ` ( J tX K ) ) <. R , S >. ) )