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 = ℤ_{\geq M}$
	txlm.m	$⊢ φ \to M \in ℤ$
	txlm.j	$⊢ φ \to J \in TopOn (X)$
	txlm.k	$⊢ φ \to K \in TopOn (Y)$
	txlm.f	$⊢ φ \to F : Z ⟶ X$
	txlm.g	$⊢ φ \to G : Z ⟶ Y$
	txlm.h	$⊢ H = (n \in Z ⟼ ⟨F (n), G (n)⟩)$
Assertion	txlm	$⊢ φ \to ((F \underset{t}{⇝} (J) R \land G \underset{t}{⇝} (K) S) \leftrightarrow H \underset{t}{⇝} (J \times_{t} K) ⟨R, S⟩)$

Proof

Step	Hyp	Ref	Expression
1		txlm.z	$⊢ Z = ℤ_{\geq M}$
2		txlm.m	$⊢ φ \to M \in ℤ$
3		txlm.j	$⊢ φ \to J \in TopOn (X)$
4		txlm.k	$⊢ φ \to K \in TopOn (Y)$
5		txlm.f	$⊢ φ \to F : Z ⟶ X$
6		txlm.g	$⊢ φ \to G : Z ⟶ Y$
7		txlm.h	$⊢ H = (n \in Z ⟼ ⟨F (n), G (n)⟩)$
8		r19.27v	$⊢ (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall u \in J ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
9		r19.28v	$⊢ ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
10	9	ralimi	$⊢ \forall u \in J ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
11	8 10	syl	$⊢ (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
12		simprl	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to w \in (J \times_{t} K)$
13		topontop	$⊢ J \in TopOn (X) \to J \in Top$
14	3 13	syl	$⊢ φ \to J \in Top$
15		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
16	4 15	syl	$⊢ φ \to K \in Top$
17		eqid	$⊢ ran (u \in J, v \in K ⟼ u \times v) = ran (u \in J, v \in K ⟼ u \times v)$
18	17	txval	$⊢ (J \in Top \land K \in Top) \to J \times_{t} K = topGen (ran (u \in J, v \in K ⟼ u \times v))$
19	14 16 18	syl2anc	$⊢ φ \to J \times_{t} K = topGen (ran (u \in J, v \in K ⟼ u \times v))$
20	19	adantr	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to J \times_{t} K = topGen (ran (u \in J, v \in K ⟼ u \times v))$
21	12 20	eleqtrd	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to w \in topGen (ran (u \in J, v \in K ⟼ u \times v))$
22		simprr	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to ⟨R, S⟩ \in w$
23		tg2	$⊢ (w \in topGen (ran (u \in J, v \in K ⟼ u \times v)) \land ⟨R, S⟩ \in w) \to \exists t \in ran (u \in J, v \in K ⟼ u \times v) (⟨R, S⟩ \in t \land t \subseteq w)$
24	21 22 23	syl2anc	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to \exists t \in ran (u \in J, v \in K ⟼ u \times v) (⟨R, S⟩ \in t \land t \subseteq w)$
25		vex	$⊢ u \in V$
26		vex	$⊢ v \in V$
27	25 26	xpex	$⊢ u \times v \in V$
28	27	rgen2w	$⊢ \forall u \in J \forall v \in K u \times v \in V$
29		eqid	$⊢ (u \in J, v \in K ⟼ u \times v) = (u \in J, v \in K ⟼ u \times v)$
30		eleq2	$⊢ t = u \times v \to (⟨R, S⟩ \in t \leftrightarrow ⟨R, S⟩ \in (u \times v))$
31		sseq1	$⊢ t = u \times v \to (t \subseteq w \leftrightarrow u \times v \subseteq w)$
32	30 31	anbi12d	$⊢ t = u \times v \to ((⟨R, S⟩ \in t \land t \subseteq w) \leftrightarrow (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w))$
33	29 32	rexrnmpo	$⊢ \forall u \in J \forall v \in K u \times v \in V \to (\exists t \in ran (u \in J, v \in K ⟼ u \times v) (⟨R, S⟩ \in t \land t \subseteq w) \leftrightarrow \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w))$
34	28 33	ax-mp	$⊢ \exists t \in ran (u \in J, v \in K ⟼ u \times v) (⟨R, S⟩ \in t \land t \subseteq w) \leftrightarrow \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)$
35	24 34	sylib	$⊢ (φ \land (w \in (J \times_{t} K) \land ⟨R, S⟩ \in w)) \to \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)$
36	35	ex	$⊢ φ \to ((w \in (J \times_{t} K) \land ⟨R, S⟩ \in w) \to \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w))$
37		r19.29	$⊢ (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists u \in J (\forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w))$
38		r19.29	$⊢ (\forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists v \in K (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w))$
39		simprl	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to ⟨R, S⟩ \in (u \times v)$
40		opelxp	$⊢ ⟨R, S⟩ \in (u \times v) \leftrightarrow (R \in u \land S \in v)$
41	39 40	sylib	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to (R \in u \land S \in v)$
42		pm2.27	$⊢ R \in u \to ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)$
43		pm2.27	$⊢ S \in v \to ((S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v) \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)$
44	42 43	im2anan9	$⊢ (R \in u \land S \in v) \to (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \land \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
45	41 44	syl	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \land \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
46	1	rexanuz2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in u \land G (k) \in v) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \land \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)$
47	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
48		opelxpi	$⊢ (F (k) \in u \land G (k) \in v) \to ⟨F (k), G (k)⟩ \in (u \times v)$
49		fveq2	$⊢ n = k \to F (n) = F (k)$
50		fveq2	$⊢ n = k \to G (n) = G (k)$
51	49 50	opeq12d	$⊢ n = k \to ⟨F (n), G (n)⟩ = ⟨F (k), G (k)⟩$
52		opex	$⊢ ⟨F (k), G (k)⟩ \in V$
53	51 7 52	fvmpt	$⊢ k \in Z \to H (k) = ⟨F (k), G (k)⟩$
54	53	eleq1d	$⊢ k \in Z \to (H (k) \in (u \times v) \leftrightarrow ⟨F (k), G (k)⟩ \in (u \times v))$
55	48 54	imbitrrid	$⊢ k \in Z \to ((F (k) \in u \land G (k) \in v) \to H (k) \in (u \times v))$
56	55	adantl	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land k \in Z) \to ((F (k) \in u \land G (k) \in v) \to H (k) \in (u \times v))$
57		simplrr	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land k \in Z) \to u \times v \subseteq w$
58	57	sseld	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land k \in Z) \to (H (k) \in (u \times v) \to H (k) \in w)$
59	56 58	syld	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land k \in Z) \to ((F (k) \in u \land G (k) \in v) \to H (k) \in w)$
60	47 59	sylan2	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land (j \in Z \land k \in ℤ_{\geq j})) \to ((F (k) \in u \land G (k) \in v) \to H (k) \in w)$
61	60	anassrs	$⊢ (((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((F (k) \in u \land G (k) \in v) \to H (k) \in w)$
62	61	ralimdva	$⊢ ((((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in u \land G (k) \in v) \to \forall k \in ℤ_{\geq j} H (k) \in w)$
63	62	reximdva	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in u \land G (k) \in v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
64	46 63	biimtrrid	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to ((\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \land \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
65	45 64	syld	$⊢ (((φ \land u \in J) \land v \in K) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
66	65	ex	$⊢ ((φ \land u \in J) \land v \in K) \to ((⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w) \to (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
67	66	impcomd	$⊢ ((φ \land u \in J) \land v \in K) \to ((((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
68	67	rexlimdva	$⊢ (φ \land u \in J) \to (\exists v \in K (((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
69	38 68	syl5	$⊢ (φ \land u \in J) \to ((\forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
70	69	rexlimdva	$⊢ φ \to (\exists u \in J (\forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
71	37 70	syl5	$⊢ φ \to ((\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \land \exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)$
72	71	expcomd	$⊢ φ \to (\exists u \in J \exists v \in K (⟨R, S⟩ \in (u \times v) \land u \times v \subseteq w) \to (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
73	36 72	syld	$⊢ φ \to ((w \in (J \times_{t} K) \land ⟨R, S⟩ \in w) \to (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
74	73	expdimp	$⊢ (φ \land w \in (J \times_{t} K)) \to (⟨R, S⟩ \in w \to (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
75	74	com23	$⊢ (φ \land w \in (J \times_{t} K)) \to (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
76	75	ralrimdva	$⊢ φ \to (\forall u \in J \forall v \in K ((R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
77	11 76	syl5	$⊢ φ \to ((\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
78	77	adantr	$⊢ (φ \land (R \in X \land S \in Y)) \to ((\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \to \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
79	14	adantr	$⊢ (φ \land (S \in Y \land u \in J)) \to J \in Top$
80	16	adantr	$⊢ (φ \land (S \in Y \land u \in J)) \to K \in Top$
81		simprr	$⊢ (φ \land (S \in Y \land u \in J)) \to u \in J$
82		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
83	4 82	syl	$⊢ φ \to Y \in K$
84	83	adantr	$⊢ (φ \land (S \in Y \land u \in J)) \to Y \in K$
85		txopn	$⊢ ((J \in Top \land K \in Top) \land (u \in J \land Y \in K)) \to u \times Y \in (J \times_{t} K)$
86	79 80 81 84 85	syl22anc	$⊢ (φ \land (S \in Y \land u \in J)) \to u \times Y \in (J \times_{t} K)$
87		eleq2	$⊢ w = u \times Y \to (⟨R, S⟩ \in w \leftrightarrow ⟨R, S⟩ \in (u \times Y))$
88		eleq2	$⊢ w = u \times Y \to (H (k) \in w \leftrightarrow H (k) \in (u \times Y))$
89	88	rexralbidv	$⊢ w = u \times Y \to (\exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y))$
90	87 89	imbi12d	$⊢ w = u \times Y \to ((⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \leftrightarrow (⟨R, S⟩ \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y)))$
91	90	rspcv	$⊢ u \times Y \in (J \times_{t} K) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (⟨R, S⟩ \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y)))$
92	86 91	syl	$⊢ (φ \land (S \in Y \land u \in J)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (⟨R, S⟩ \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y)))$
93		simprl	$⊢ (φ \land (S \in Y \land u \in J)) \to S \in Y$
94		opelxpi	$⊢ (R \in u \land S \in Y) \to ⟨R, S⟩ \in (u \times Y)$
95	93 94	sylan2	$⊢ (R \in u \land (φ \land (S \in Y \land u \in J))) \to ⟨R, S⟩ \in (u \times Y)$
96	95	expcom	$⊢ (φ \land (S \in Y \land u \in J)) \to (R \in u \to ⟨R, S⟩ \in (u \times Y))$
97	53	eleq1d	$⊢ k \in Z \to (H (k) \in (u \times Y) \leftrightarrow ⟨F (k), G (k)⟩ \in (u \times Y))$
98		opelxp1	$⊢ ⟨F (k), G (k)⟩ \in (u \times Y) \to F (k) \in u$
99	97 98	syl6bi	$⊢ k \in Z \to (H (k) \in (u \times Y) \to F (k) \in u)$
100	47 99	syl	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (H (k) \in (u \times Y) \to F (k) \in u)$
101	100	ralimdva	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} H (k) \in (u \times Y) \to \forall k \in ℤ_{\geq j} F (k) \in u)$
102	101	reximia	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u$
103	102	a1i	$⊢ (φ \land (S \in Y \land u \in J)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)$
104	96 103	imim12d	$⊢ (φ \land (S \in Y \land u \in J)) \to ((⟨R, S⟩ \in (u \times Y) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (u \times Y)) \to (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
105	92 104	syld	$⊢ (φ \land (S \in Y \land u \in J)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
106	105	anassrs	$⊢ ((φ \land S \in Y) \land u \in J) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
107	106	ralrimdva	$⊢ (φ \land S \in Y) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to \forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
108	107	adantrl	$⊢ (φ \land (R \in X \land S \in Y)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to \forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u))$
109	14	adantr	$⊢ (φ \land (R \in X \land v \in K)) \to J \in Top$
110	16	adantr	$⊢ (φ \land (R \in X \land v \in K)) \to K \in Top$
111		toponmax	$⊢ J \in TopOn (X) \to X \in J$
112	3 111	syl	$⊢ φ \to X \in J$
113	112	adantr	$⊢ (φ \land (R \in X \land v \in K)) \to X \in J$
114		simprr	$⊢ (φ \land (R \in X \land v \in K)) \to v \in K$
115		txopn	$⊢ ((J \in Top \land K \in Top) \land (X \in J \land v \in K)) \to X \times v \in (J \times_{t} K)$
116	109 110 113 114 115	syl22anc	$⊢ (φ \land (R \in X \land v \in K)) \to X \times v \in (J \times_{t} K)$
117		eleq2	$⊢ w = X \times v \to (⟨R, S⟩ \in w \leftrightarrow ⟨R, S⟩ \in (X \times v))$
118		eleq2	$⊢ w = X \times v \to (H (k) \in w \leftrightarrow H (k) \in (X \times v))$
119	118	rexralbidv	$⊢ w = X \times v \to (\exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v))$
120	117 119	imbi12d	$⊢ w = X \times v \to ((⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \leftrightarrow (⟨R, S⟩ \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v)))$
121	120	rspcv	$⊢ X \times v \in (J \times_{t} K) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (⟨R, S⟩ \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v)))$
122	116 121	syl	$⊢ (φ \land (R \in X \land v \in K)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (⟨R, S⟩ \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v)))$
123		opelxpi	$⊢ (R \in X \land S \in v) \to ⟨R, S⟩ \in (X \times v)$
124	123	ex	$⊢ R \in X \to (S \in v \to ⟨R, S⟩ \in (X \times v))$
125	124	ad2antrl	$⊢ (φ \land (R \in X \land v \in K)) \to (S \in v \to ⟨R, S⟩ \in (X \times v))$
126	53	eleq1d	$⊢ k \in Z \to (H (k) \in (X \times v) \leftrightarrow ⟨F (k), G (k)⟩ \in (X \times v))$
127		opelxp2	$⊢ ⟨F (k), G (k)⟩ \in (X \times v) \to G (k) \in v$
128	126 127	syl6bi	$⊢ k \in Z \to (H (k) \in (X \times v) \to G (k) \in v)$
129	47 128	syl	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (H (k) \in (X \times v) \to G (k) \in v)$
130	129	ralimdva	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} H (k) \in (X \times v) \to \forall k \in ℤ_{\geq j} G (k) \in v)$
131	130	reximia	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v$
132	131	a1i	$⊢ (φ \land (R \in X \land v \in K)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)$
133	125 132	imim12d	$⊢ (φ \land (R \in X \land v \in K)) \to ((⟨R, S⟩ \in (X \times v) \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in (X \times v)) \to (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
134	122 133	syld	$⊢ (φ \land (R \in X \land v \in K)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
135	134	anassrs	$⊢ ((φ \land R \in X) \land v \in K) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
136	135	ralrimdva	$⊢ (φ \land R \in X) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
137	136	adantrr	$⊢ (φ \land (R \in X \land S \in Y)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))$
138	108 137	jcad	$⊢ (φ \land (R \in X \land S \in Y)) \to (\forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w) \to (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)))$
139	78 138	impbid	$⊢ (φ \land (R \in X \land S \in Y)) \to ((\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)) \leftrightarrow \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
140	139	pm5.32da	$⊢ φ \to (((R \in X \land S \in Y) \land (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))) \leftrightarrow ((R \in X \land S \in Y) \land \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)))$
141		opelxp	$⊢ ⟨R, S⟩ \in (X \times Y) \leftrightarrow (R \in X \land S \in Y)$
142	141	anbi1i	$⊢ (⟨R, S⟩ \in (X \times Y) \land \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)) \leftrightarrow ((R \in X \land S \in Y) \land \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w))$
143	140 142	bitr4di	$⊢ φ \to (((R \in X \land S \in Y) \land (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))) \leftrightarrow (⟨R, S⟩ \in (X \times Y) \land \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)))$
144		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
145	3 1 2 5 144	lmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) R \leftrightarrow (R \in X \land \forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)))$
146		eqidd	$⊢ (φ \land k \in Z) \to G (k) = G (k)$
147	4 1 2 6 146	lmbrf	$⊢ φ \to (G \underset{t}{⇝} (K) S \leftrightarrow (S \in Y \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)))$
148	145 147	anbi12d	$⊢ φ \to ((F \underset{t}{⇝} (J) R \land G \underset{t}{⇝} (K) S) \leftrightarrow ((R \in X \land \forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \land (S \in Y \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))))$
149		an4	$⊢ ((R \in X \land \forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)) \land (S \in Y \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))) \leftrightarrow ((R \in X \land S \in Y) \land (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v)))$
150	148 149	bitrdi	$⊢ φ \to ((F \underset{t}{⇝} (J) R \land G \underset{t}{⇝} (K) S) \leftrightarrow ((R \in X \land S \in Y) \land (\forall u \in J (R \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \land \forall v \in K (S \in v \to \exists j \in Z \forall k \in ℤ_{\geq j} G (k) \in v))))$
151		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
152	3 4 151	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
153	5	ffvelcdmda	$⊢ (φ \land n \in Z) \to F (n) \in X$
154	6	ffvelcdmda	$⊢ (φ \land n \in Z) \to G (n) \in Y$
155	153 154	opelxpd	$⊢ (φ \land n \in Z) \to ⟨F (n), G (n)⟩ \in (X \times Y)$
156	155 7	fmptd	$⊢ φ \to H : Z ⟶ X \times Y$
157		eqidd	$⊢ (φ \land k \in Z) \to H (k) = H (k)$
158	152 1 2 156 157	lmbrf	$⊢ φ \to (H \underset{t}{⇝} (J \times_{t} K) ⟨R, S⟩ \leftrightarrow (⟨R, S⟩ \in (X \times Y) \land \forall w \in (J \times_{t} K) (⟨R, S⟩ \in w \to \exists j \in Z \forall k \in ℤ_{\geq j} H (k) \in w)))$
159	143 150 158	3bitr4d	$⊢ φ \to ((F \underset{t}{⇝} (J) R \land G \underset{t}{⇝} (K) S) \leftrightarrow H \underset{t}{⇝} (J \times_{t} K) ⟨R, S⟩)$

Metamath Proof Explorer

Theorem txlm

Proof