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 syl5bir
 |-  ( 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( ( 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 syl5bb
 |-  ( ( 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 ffvelrnda
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
146 5 ffvelrnda
 |-  ( ( 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 ) ) ) )