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	$⊢ φ \to J \in TopOn (X)$
	txflf.k	$⊢ φ \to K \in TopOn (Y)$
	txflf.l	$⊢ φ \to L \in Fil (Z)$
	txflf.f	$⊢ φ \to F : Z ⟶ X$
	txflf.g	$⊢ φ \to G : Z ⟶ Y$
	txflf.h	$⊢ H = (n \in Z ⟼ ⟨F (n), G (n)⟩)$
Assertion	txflf	$⊢ φ \to (⟨R, S⟩ \in ((J \times_{t} K) fLimf L) (H) \leftrightarrow (R \in (J fLimf L) (F) \land S \in (K fLimf L) (G)))$

Proof

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

Metamath Proof Explorer

Theorem txflf

Proof