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

Metamath Proof Explorer

Theorem txflf

Proof