Metamath Proof Explorer

Theorem txflf

Description: Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses txflf.j 
|- ( ph -> J e. ( TopOn ` X ) )
txflf.k 
|- ( ph -> K e. ( TopOn ` Y ) )
txflf.l 
|- ( ph -> L e. ( Fil ` Z ) )
txflf.f 
|- ( ph -> F : Z --> X )
txflf.g 
|- ( ph -> G : Z --> Y )
txflf.h 
|- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )
Assertion txflf 
|- ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` H ) <-> ( R e. ( ( J fLimf L ) ` F ) /\ S e. ( ( K fLimf L ) ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 txflf.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 txflf.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 txflf.l 
 |-  ( ph -> L e. ( Fil ` Z ) )
4 txflf.f 
 |-  ( ph -> F : Z --> X )
5 txflf.g 
 |-  ( ph -> G : Z --> Y )
6 txflf.h 
 |-  H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )
7 vex 
 |-  u e. _V
8 vex 
 |-  v e. _V
9 7 8 xpex 
 |-  ( u X. v ) e. _V
10 9 rgen2w 
 |-  A. u e. J A. v e. K ( u X. v ) e. _V
11 eqid 
 |-  ( u e. J , v e. K |-> ( u X. v ) ) = ( u e. J , v e. K |-> ( u X. v ) )
12 eleq2 
 |-  ( z = ( u X. v ) -> ( <. R , S >. e. z <-> <. R , S >. e. ( u X. v ) ) )
13 sseq2 
 |-  ( z = ( u X. v ) -> ( ( H " h ) C_ z <-> ( H " h ) C_ ( u X. v ) ) )
14 13 rexbidv 
 |-  ( z = ( u X. v ) -> ( E. h e. L ( H " h ) C_ z <-> E. h e. L ( H " h ) C_ ( u X. v ) ) )
15 12 14 imbi12d 
 |-  ( z = ( u X. v ) -> ( ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) <-> ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) ) )
16 11 15 ralrnmpo 
 |-  ( A. u e. J A. v e. K ( u X. v ) e. _V -> ( A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) <-> A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) ) )
17 10 16 ax-mp 
 |-  ( A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) <-> A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) )
18 opelxp 
 |-  ( <. R , S >. e. ( u X. v ) <-> ( R e. u /\ S e. v ) )
19 18 biancomi 
 |-  ( <. R , S >. e. ( u X. v ) <-> ( S e. v /\ R e. u ) )
20 19 a1i 
 |-  ( ph -> ( <. R , S >. e. ( u X. v ) <-> ( S e. v /\ R e. u ) ) )
21 r19.40 
 |-  ( E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) -> ( E. h e. L A. n e. h ( F ` n ) e. u /\ E. h e. L A. n e. h ( G ` n ) e. v ) )
22 raleq 
 |-  ( h = f -> ( A. n e. h ( F ` n ) e. u <-> A. n e. f ( F ` n ) e. u ) )
23 22 cbvrexvw 
 |-  ( E. h e. L A. n e. h ( F ` n ) e. u <-> E. f e. L A. n e. f ( F ` n ) e. u )
24 raleq 
 |-  ( h = g -> ( A. n e. h ( G ` n ) e. v <-> A. n e. g ( G ` n ) e. v ) )
25 24 cbvrexvw 
 |-  ( E. h e. L A. n e. h ( G ` n ) e. v <-> E. g e. L A. n e. g ( G ` n ) e. v )
26 23 25 anbi12i 
 |-  ( ( E. h e. L A. n e. h ( F ` n ) e. u /\ E. h e. L A. n e. h ( G ` n ) e. v ) <-> ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) )
27 21 26 sylib 
 |-  ( E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) -> ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) )
28 reeanv 
 |-  ( E. f e. L E. g e. L ( A. n e. f ( F ` n ) e. u /\ A. n e. g ( G ` n ) e. v ) <-> ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) )
29 filin 
 |-  ( ( L e. ( Fil ` Z ) /\ f e. L /\ g e. L ) -> ( f i^i g ) e. L )
30 29 3expb 
 |-  ( ( L e. ( Fil ` Z ) /\ ( f e. L /\ g e. L ) ) -> ( f i^i g ) e. L )
31 3 30 sylan 
 |-  ( ( ph /\ ( f e. L /\ g e. L ) ) -> ( f i^i g ) e. L )
32 inss1 
 |-  ( f i^i g ) C_ f
33 ssralv 
 |-  ( ( f i^i g ) C_ f -> ( A. n e. f ( F ` n ) e. u -> A. n e. ( f i^i g ) ( F ` n ) e. u ) )
34 32 33 ax-mp 
 |-  ( A. n e. f ( F ` n ) e. u -> A. n e. ( f i^i g ) ( F ` n ) e. u )
35 inss2 
 |-  ( f i^i g ) C_ g
36 ssralv 
 |-  ( ( f i^i g ) C_ g -> ( A. n e. g ( G ` n ) e. v -> A. n e. ( f i^i g ) ( G ` n ) e. v ) )
37 35 36 ax-mp 
 |-  ( A. n e. g ( G ` n ) e. v -> A. n e. ( f i^i g ) ( G ` n ) e. v )
38 34 37 anim12i 
 |-  ( ( A. n e. f ( F ` n ) e. u /\ A. n e. g ( G ` n ) e. v ) -> ( A. n e. ( f i^i g ) ( F ` n ) e. u /\ A. n e. ( f i^i g ) ( G ` n ) e. v ) )
39 raleq 
 |-  ( h = ( f i^i g ) -> ( A. n e. h ( F ` n ) e. u <-> A. n e. ( f i^i g ) ( F ` n ) e. u ) )
40 raleq 
 |-  ( h = ( f i^i g ) -> ( A. n e. h ( G ` n ) e. v <-> A. n e. ( f i^i g ) ( G ` n ) e. v ) )
41 39 40 anbi12d 
 |-  ( h = ( f i^i g ) -> ( ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) <-> ( A. n e. ( f i^i g ) ( F ` n ) e. u /\ A. n e. ( f i^i g ) ( G ` n ) e. v ) ) )
42 41 rspcev 
 |-  ( ( ( f i^i g ) e. L /\ ( A. n e. ( f i^i g ) ( F ` n ) e. u /\ A. n e. ( f i^i g ) ( G ` n ) e. v ) ) -> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) )
43 31 38 42 syl2an 
 |-  ( ( ( ph /\ ( f e. L /\ g e. L ) ) /\ ( A. n e. f ( F ` n ) e. u /\ A. n e. g ( G ` n ) e. v ) ) -> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) )
44 43 ex 
 |-  ( ( ph /\ ( f e. L /\ g e. L ) ) -> ( ( A. n e. f ( F ` n ) e. u /\ A. n e. g ( G ` n ) e. v ) -> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) ) )
45 44 rexlimdvva 
 |-  ( ph -> ( E. f e. L E. g e. L ( A. n e. f ( F ` n ) e. u /\ A. n e. g ( G ` n ) e. v ) -> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) ) )
46 28 45 biimtrrid 
 |-  ( ph -> ( ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) -> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) ) )
47 27 46 impbid2 
 |-  ( ph -> ( E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) <-> ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) ) )
48 df-ima 
 |-  ( H " h ) = ran ( H |` h )
49 filelss 
 |-  ( ( L e. ( Fil ` Z ) /\ h e. L ) -> h C_ Z )
50 3 49 sylan 
 |-  ( ( ph /\ h e. L ) -> h C_ Z )
51 6 reseq1i 
 |-  ( H |` h ) = ( ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) |` h )
52 resmpt 
 |-  ( h C_ Z -> ( ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) |` h ) = ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) )
53 51 52 eqtrid 
 |-  ( h C_ Z -> ( H |` h ) = ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) )
54 50 53 syl 
 |-  ( ( ph /\ h e. L ) -> ( H |` h ) = ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) )
55 54 rneqd 
 |-  ( ( ph /\ h e. L ) -> ran ( H |` h ) = ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) )
56 48 55 eqtrid 
 |-  ( ( ph /\ h e. L ) -> ( H " h ) = ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) )
57 56 sseq1d 
 |-  ( ( ph /\ h e. L ) -> ( ( H " h ) C_ ( u X. v ) <-> ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) C_ ( u X. v ) ) )
58 opelxp 
 |-  ( <. ( F ` n ) , ( G ` n ) >. e. ( u X. v ) <-> ( ( F ` n ) e. u /\ ( G ` n ) e. v ) )
59 58 ralbii 
 |-  ( A. n e. h <. ( F ` n ) , ( G ` n ) >. e. ( u X. v ) <-> A. n e. h ( ( F ` n ) e. u /\ ( G ` n ) e. v ) )
60 eqid 
 |-  ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) = ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. )
61 60 fmpt 
 |-  ( A. n e. h <. ( F ` n ) , ( G ` n ) >. e. ( u X. v ) <-> ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) : h --> ( u X. v ) )
62 opex 
 |-  <. ( F ` n ) , ( G ` n ) >. e. _V
63 62 60 fnmpti 
 |-  ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) Fn h
64 df-f 
 |-  ( ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) : h --> ( u X. v ) <-> ( ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) Fn h /\ ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) C_ ( u X. v ) ) )
65 63 64 mpbiran 
 |-  ( ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) : h --> ( u X. v ) <-> ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) C_ ( u X. v ) )
66 61 65 bitri 
 |-  ( A. n e. h <. ( F ` n ) , ( G ` n ) >. e. ( u X. v ) <-> ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) C_ ( u X. v ) )
67 r19.26 
 |-  ( A. n e. h ( ( F ` n ) e. u /\ ( G ` n ) e. v ) <-> ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) )
68 59 66 67 3bitr3i 
 |-  ( ran ( n e. h |-> <. ( F ` n ) , ( G ` n ) >. ) C_ ( u X. v ) <-> ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) )
69 57 68 bitrdi 
 |-  ( ( ph /\ h e. L ) -> ( ( H " h ) C_ ( u X. v ) <-> ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) ) )
70 69 rexbidva 
 |-  ( ph -> ( E. h e. L ( H " h ) C_ ( u X. v ) <-> E. h e. L ( A. n e. h ( F ` n ) e. u /\ A. n e. h ( G ` n ) e. v ) ) )
71 4 adantr 
 |-  ( ( ph /\ f e. L ) -> F : Z --> X )
72 71 ffund 
 |-  ( ( ph /\ f e. L ) -> Fun F )
73 filelss 
 |-  ( ( L e. ( Fil ` Z ) /\ f e. L ) -> f C_ Z )
74 3 73 sylan 
 |-  ( ( ph /\ f e. L ) -> f C_ Z )
75 71 fdmd 
 |-  ( ( ph /\ f e. L ) -> dom F = Z )
76 74 75 sseqtrrd 
 |-  ( ( ph /\ f e. L ) -> f C_ dom F )
77 funimass4 
 |-  ( ( Fun F /\ f C_ dom F ) -> ( ( F " f ) C_ u <-> A. n e. f ( F ` n ) e. u ) )
78 72 76 77 syl2anc 
 |-  ( ( ph /\ f e. L ) -> ( ( F " f ) C_ u <-> A. n e. f ( F ` n ) e. u ) )
79 78 rexbidva 
 |-  ( ph -> ( E. f e. L ( F " f ) C_ u <-> E. f e. L A. n e. f ( F ` n ) e. u ) )
80 5 adantr 
 |-  ( ( ph /\ g e. L ) -> G : Z --> Y )
81 80 ffund 
 |-  ( ( ph /\ g e. L ) -> Fun G )
82 filelss 
 |-  ( ( L e. ( Fil ` Z ) /\ g e. L ) -> g C_ Z )
83 3 82 sylan 
 |-  ( ( ph /\ g e. L ) -> g C_ Z )
84 80 fdmd 
 |-  ( ( ph /\ g e. L ) -> dom G = Z )
85 83 84 sseqtrrd 
 |-  ( ( ph /\ g e. L ) -> g C_ dom G )
86 funimass4 
 |-  ( ( Fun G /\ g C_ dom G ) -> ( ( G " g ) C_ v <-> A. n e. g ( G ` n ) e. v ) )
87 81 85 86 syl2anc 
 |-  ( ( ph /\ g e. L ) -> ( ( G " g ) C_ v <-> A. n e. g ( G ` n ) e. v ) )
88 87 rexbidva 
 |-  ( ph -> ( E. g e. L ( G " g ) C_ v <-> E. g e. L A. n e. g ( G ` n ) e. v ) )
89 79 88 anbi12d 
 |-  ( ph -> ( ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> ( E. f e. L A. n e. f ( F ` n ) e. u /\ E. g e. L A. n e. g ( G ` n ) e. v ) ) )
90 47 70 89 3bitr4d 
 |-  ( ph -> ( E. h e. L ( H " h ) C_ ( u X. v ) <-> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
91 20 90 imbi12d 
 |-  ( ph -> ( ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> ( ( S e. v /\ R e. u ) -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) )
92 impexp 
 |-  ( ( ( S e. v /\ R e. u ) -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) <-> ( S e. v -> ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) )
93 91 92 bitrdi 
 |-  ( ph -> ( ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> ( S e. v -> ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) ) )
94 93 ralbidv 
 |-  ( ph -> ( A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> A. v e. K ( S e. v -> ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) ) )
95 eleq2 
 |-  ( x = v -> ( S e. x <-> S e. v ) )
96 95 ralrab 
 |-  ( A. v e. { x e. K | S e. x } ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) <-> A. v e. K ( S e. v -> ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) )
97 r19.21v 
 |-  ( A. v e. { x e. K | S e. x } ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) <-> ( R e. u -> A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
98 96 97 bitr3i 
 |-  ( A. v e. K ( S e. v -> ( R e. u -> ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) <-> ( R e. u -> A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
99 94 98 bitrdi 
 |-  ( ph -> ( A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> ( R e. u -> A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) )
100 99 ralbidv 
 |-  ( ph -> ( A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> A. u e. J ( R e. u -> A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) ) )
101 eleq2 
 |-  ( x = u -> ( R e. x <-> R e. u ) )
102 101 ralrab 
 |-  ( A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> A. u e. J ( R e. u -> A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
103 100 102 bitr4di 
 |-  ( ph -> ( A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
104 103 adantr 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) ) )
105 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
106 1 105 syl 
 |-  ( ph -> X e. J )
107 eleq2 
 |-  ( x = X -> ( R e. x <-> R e. X ) )
108 107 rspcev 
 |-  ( ( X e. J /\ R e. X ) -> E. x e. J R e. x )
109 rabn0 
 |-  ( { x e. J | R e. x } =/= (/) <-> E. x e. J R e. x )
110 108 109 sylibr 
 |-  ( ( X e. J /\ R e. X ) -> { x e. J | R e. x } =/= (/) )
111 106 110 sylan 
 |-  ( ( ph /\ R e. X ) -> { x e. J | R e. x } =/= (/) )
112 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
113 2 112 syl 
 |-  ( ph -> Y e. K )
114 eleq2 
 |-  ( x = Y -> ( S e. x <-> S e. Y ) )
115 114 rspcev 
 |-  ( ( Y e. K /\ S e. Y ) -> E. x e. K S e. x )
116 rabn0 
 |-  ( { x e. K | S e. x } =/= (/) <-> E. x e. K S e. x )
117 115 116 sylibr 
 |-  ( ( Y e. K /\ S e. Y ) -> { x e. K | S e. x } =/= (/) )
118 113 117 sylan 
 |-  ( ( ph /\ S e. Y ) -> { x e. K | S e. x } =/= (/) )
119 111 118 anim12dan 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( { x e. J | R e. x } =/= (/) /\ { x e. K | S e. x } =/= (/) ) )
120 r19.28zv 
 |-  ( { x e. K | S e. x } =/= (/) -> ( A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> ( E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
121 120 ralbidv 
 |-  ( { x e. K | S e. x } =/= (/) -> ( A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> A. u e. { x e. J | R e. x } ( E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
122 r19.27zv 
 |-  ( { x e. J | R e. x } =/= (/) -> ( A. u e. { x e. J | R e. x } ( E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) <-> ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
123 121 122 sylan9bbr 
 |-  ( ( { x e. J | R e. x } =/= (/) /\ { x e. K | S e. x } =/= (/) ) -> ( A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
124 119 123 syl 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. u e. { x e. J | R e. x } A. v e. { x e. K | S e. x } ( E. f e. L ( F " f ) C_ u /\ E. g e. L ( G " g ) C_ v ) <-> ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
125 104 124 bitrd 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) ) )
126 101 ralrab 
 |-  ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u <-> A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) )
127 95 ralrab 
 |-  ( A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v <-> A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) )
128 126 127 anbi12i 
 |-  ( ( A. u e. { x e. J | R e. x } E. f e. L ( F " f ) C_ u /\ A. v e. { x e. K | S e. x } E. g e. L ( G " g ) C_ v ) <-> ( A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) )
129 125 128 bitrdi 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. u e. J A. v e. K ( <. R , S >. e. ( u X. v ) -> E. h e. L ( H " h ) C_ ( u X. v ) ) <-> ( A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) )
130 17 129 bitrid 
 |-  ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) <-> ( A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) )
131 130 pm5.32da 
 |-  ( ph -> ( ( ( R e. X /\ S e. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) ) )
132 opelxp 
 |-  ( <. R , S >. e. ( X X. Y ) <-> ( R e. X /\ S e. Y ) )
133 132 anbi1i 
 |-  ( ( <. R , S >. e. ( X X. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) <-> ( ( R e. X /\ S e. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) )
134 an4 
 |-  ( ( ( R e. X /\ A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) )
135 131 133 134 3bitr4g 
 |-  ( ph -> ( ( <. R , S >. e. ( X X. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) <-> ( ( R e. X /\ A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) ) )
136 eqid 
 |-  ran ( u e. J , v e. K |-> ( u X. v ) ) = ran ( u e. J , v e. K |-> ( u X. v ) )
137 136 txval 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
138 1 2 137 syl2anc 
 |-  ( ph -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) )
139 138 oveq1d 
 |-  ( ph -> ( ( J tX K ) fLimf L ) = ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) fLimf L ) )
140 139 fveq1d 
 |-  ( ph -> ( ( ( J tX K ) fLimf L ) ` H ) = ( ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) fLimf L ) ` H ) )
141 140 eleq2d 
 |-  ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` H ) <-> <. R , S >. e. ( ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) fLimf L ) ` H ) ) )
142 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
143 1 2 142 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
144 138 143 eqeltrrd 
 |-  ( ph -> ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) e. ( TopOn ` ( X X. Y ) ) )
145 4 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
146 5 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) e. Y )
147 145 146 opelxpd 
 |-  ( ( ph /\ n e. Z ) -> <. ( F ` n ) , ( G ` n ) >. e. ( X X. Y ) )
148 147 6 fmptd 
 |-  ( ph -> H : Z --> ( X X. Y ) )
149 eqid 
 |-  ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) )
150 149 flftg 
 |-  ( ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( Fil ` Z ) /\ H : Z --> ( X X. Y ) ) -> ( <. R , S >. e. ( ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) fLimf L ) ` H ) <-> ( <. R , S >. e. ( X X. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) ) )
151 144 3 148 150 syl3anc 
 |-  ( ph -> ( <. R , S >. e. ( ( ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) fLimf L ) ` H ) <-> ( <. R , S >. e. ( X X. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) ) )
152 141 151 bitrd 
 |-  ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` H ) <-> ( <. R , S >. e. ( X X. Y ) /\ A. z e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. z -> E. h e. L ( H " h ) C_ z ) ) ) )
153 isflf 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Z ) /\ F : Z --> X ) -> ( R e. ( ( J fLimf L ) ` F ) <-> ( R e. X /\ A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) ) ) )
154 1 3 4 153 syl3anc 
 |-  ( ph -> ( R e. ( ( J fLimf L ) ` F ) <-> ( R e. X /\ A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) ) ) )
155 isflf 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( Fil ` Z ) /\ G : Z --> Y ) -> ( S e. ( ( K fLimf L ) ` G ) <-> ( S e. Y /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) )
156 2 3 5 155 syl3anc 
 |-  ( ph -> ( S e. ( ( K fLimf L ) ` G ) <-> ( S e. Y /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) )
157 154 156 anbi12d 
 |-  ( ph -> ( ( R e. ( ( J fLimf L ) ` F ) /\ S e. ( ( K fLimf L ) ` G ) ) <-> ( ( R e. X /\ A. u e. J ( R e. u -> E. f e. L ( F " f ) C_ u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. g e. L ( G " g ) C_ v ) ) ) ) )
158 135 152 157 3bitr4d 
 |-  ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` H ) <-> ( R e. ( ( J fLimf L ) ` F ) /\ S e. ( ( K fLimf L ) ` G ) ) ) )