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 syl5ibr
 |-  ( 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 syl5bir
 |-  ( ( ( ( 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 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 ffvelrnda
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
154 6 ffvelrnda
 |-  ( ( 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 >. ) )