tx1stc

Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	tx1stc	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to R \times_{t} S \in 1^{st} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		1stctop	$⊢ R \in 1^{st} 𝜔 \to R \in Top$
2		1stctop	$⊢ S \in 1^{st} 𝜔 \to S \in Top$
3		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
4	1 2 3	syl2an	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to R \times_{t} S \in Top$
5		eqid	$⊢ ⋃ R = ⋃ R$
6	5	1stcclb	$⊢ (R \in 1^{st} 𝜔 \land u \in ⋃ R) \to \exists a \in 𝒫 R (a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)))$
7	6	ad2ant2r	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to \exists a \in 𝒫 R (a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)))$
8		eqid	$⊢ ⋃ S = ⋃ S$
9	8	1stcclb	$⊢ (S \in 1^{st} 𝜔 \land v \in ⋃ S) \to \exists b \in 𝒫 S (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))$
10	9	ad2ant2l	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to \exists b \in 𝒫 S (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))$
11		reeanv	$⊢ \exists a \in 𝒫 R \exists b \in 𝒫 S ((a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \leftrightarrow (\exists a \in 𝒫 R (a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land \exists b \in 𝒫 S (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))$
12		an4	$⊢ ((a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \leftrightarrow ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))$
13		txopn	$⊢ ((R \in Top \land S \in Top) \land (m \in R \land n \in S)) \to m \times n \in (R \times_{t} S)$
14	13	ralrimivva	$⊢ (R \in Top \land S \in Top) \to \forall m \in R \forall n \in S m \times n \in (R \times_{t} S)$
15	1 2 14	syl2an	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to \forall m \in R \forall n \in S m \times n \in (R \times_{t} S)$
16	15	adantr	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to \forall m \in R \forall n \in S m \times n \in (R \times_{t} S)$
17		elpwi	$⊢ a \in 𝒫 R \to a \subseteq R$
18		ssralv	$⊢ a \subseteq R \to (\forall m \in R \forall n \in S m \times n \in (R \times_{t} S) \to \forall m \in a \forall n \in S m \times n \in (R \times_{t} S))$
19	17 18	syl	$⊢ a \in 𝒫 R \to (\forall m \in R \forall n \in S m \times n \in (R \times_{t} S) \to \forall m \in a \forall n \in S m \times n \in (R \times_{t} S))$
20		elpwi	$⊢ b \in 𝒫 S \to b \subseteq S$
21		ssralv	$⊢ b \subseteq S \to (\forall n \in S m \times n \in (R \times_{t} S) \to \forall n \in b m \times n \in (R \times_{t} S))$
22	20 21	syl	$⊢ b \in 𝒫 S \to (\forall n \in S m \times n \in (R \times_{t} S) \to \forall n \in b m \times n \in (R \times_{t} S))$
23	22	ralimdv	$⊢ b \in 𝒫 S \to (\forall m \in a \forall n \in S m \times n \in (R \times_{t} S) \to \forall m \in a \forall n \in b m \times n \in (R \times_{t} S))$
24	19 23	sylan9	$⊢ (a \in 𝒫 R \land b \in 𝒫 S) \to (\forall m \in R \forall n \in S m \times n \in (R \times_{t} S) \to \forall m \in a \forall n \in b m \times n \in (R \times_{t} S))$
25	16 24	mpan9	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to \forall m \in a \forall n \in b m \times n \in (R \times_{t} S)$
26		eqid	$⊢ (m \in a, n \in b ⟼ m \times n) = (m \in a, n \in b ⟼ m \times n)$
27	26	fmpo	$⊢ \forall m \in a \forall n \in b m \times n \in (R \times_{t} S) \leftrightarrow (m \in a, n \in b ⟼ m \times n) : a \times b ⟶ R \times_{t} S$
28	25 27	sylib	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to (m \in a, n \in b ⟼ m \times n) : a \times b ⟶ R \times_{t} S$
29	28	frnd	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to ran (m \in a, n \in b ⟼ m \times n) \subseteq R \times_{t} S$
30		ovex	$⊢ R \times_{t} S \in V$
31	30	elpw2	$⊢ ran (m \in a, n \in b ⟼ m \times n) \in 𝒫 (R \times_{t} S) \leftrightarrow ran (m \in a, n \in b ⟼ m \times n) \subseteq R \times_{t} S$
32	29 31	sylibr	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to ran (m \in a, n \in b ⟼ m \times n) \in 𝒫 (R \times_{t} S)$
33	32	adantr	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to ran (m \in a, n \in b ⟼ m \times n) \in 𝒫 (R \times_{t} S)$
34		omelon	$⊢ ω \in On$
35		xpct	$⊢ (a ≼ ω \land b ≼ ω) \to (a \times b) ≼ ω$
36		ondomen	$⊢ (ω \in On \land (a \times b) ≼ ω) \to a \times b \in dom card$
37	34 35 36	sylancr	$⊢ (a ≼ ω \land b ≼ ω) \to a \times b \in dom card$
38		vex	$⊢ m \in V$
39		vex	$⊢ n \in V$
40	38 39	xpex	$⊢ m \times n \in V$
41	26 40	fnmpoi	$⊢ (m \in a, n \in b ⟼ m \times n) Fn (a \times b)$
42		dffn4	$⊢ (m \in a, n \in b ⟼ m \times n) Fn (a \times b) \leftrightarrow (m \in a, n \in b ⟼ m \times n) : a \times b \underset{onto}{⟶} ran (m \in a, n \in b ⟼ m \times n)$
43	41 42	mpbi	$⊢ (m \in a, n \in b ⟼ m \times n) : a \times b \underset{onto}{⟶} ran (m \in a, n \in b ⟼ m \times n)$
44		fodomnum	$⊢ a \times b \in dom card \to ((m \in a, n \in b ⟼ m \times n) : a \times b \underset{onto}{⟶} ran (m \in a, n \in b ⟼ m \times n) \to ran (m \in a, n \in b ⟼ m \times n) ≼ (a \times b))$
45	37 43 44	mpisyl	$⊢ (a ≼ ω \land b ≼ ω) \to ran (m \in a, n \in b ⟼ m \times n) ≼ (a \times b)$
46		domtr	$⊢ (ran (m \in a, n \in b ⟼ m \times n) ≼ (a \times b) \land (a \times b) ≼ ω) \to ran (m \in a, n \in b ⟼ m \times n) ≼ ω$
47	45 35 46	syl2anc	$⊢ (a ≼ ω \land b ≼ ω) \to ran (m \in a, n \in b ⟼ m \times n) ≼ ω$
48	47	ad2antrl	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to ran (m \in a, n \in b ⟼ m \times n) ≼ ω$
49	1 2	anim12i	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to (R \in Top \land S \in Top)$
50	49	ad3antrrr	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to (R \in Top \land S \in Top)$
51		eltx	$⊢ (R \in Top \land S \in Top) \to (z \in (R \times_{t} S) \leftrightarrow \forall w \in z \exists r \in R \exists s \in S (w \in (r \times s) \land r \times s \subseteq z))$
52	50 51	syl	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to (z \in (R \times_{t} S) \leftrightarrow \forall w \in z \exists r \in R \exists s \in S (w \in (r \times s) \land r \times s \subseteq z))$
53		eleq1	$⊢ w = ⟨u, v⟩ \to (w \in (r \times s) \leftrightarrow ⟨u, v⟩ \in (r \times s))$
54	53	anbi1d	$⊢ w = ⟨u, v⟩ \to ((w \in (r \times s) \land r \times s \subseteq z) \leftrightarrow (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z))$
55	54	2rexbidv	$⊢ w = ⟨u, v⟩ \to (\exists r \in R \exists s \in S (w \in (r \times s) \land r \times s \subseteq z) \leftrightarrow \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z))$
56	55	rspccv	$⊢ \forall w \in z \exists r \in R \exists s \in S (w \in (r \times s) \land r \times s \subseteq z) \to (⟨u, v⟩ \in z \to \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z))$
57		r19.27v	$⊢ (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \to \forall r \in R ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))$
58		r19.29	$⊢ (\forall r \in R ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists r \in R (((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z))$
59		r19.29	$⊢ (\forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)) \land \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists s \in S ((v \in s \to \exists q \in b (v \in q \land q \subseteq s)) \land (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z))$
60		opelxp	$⊢ ⟨u, v⟩ \in (r \times s) \leftrightarrow (u \in r \land v \in s)$
61		pm3.35	$⊢ (u \in r \land (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \to \exists p \in a (u \in p \land p \subseteq r)$
62		pm3.35	$⊢ (v \in s \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \to \exists q \in b (v \in q \land q \subseteq s)$
63	61 62	anim12i	$⊢ ((u \in r \land (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land (v \in s \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to (\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s))$
64	63	an4s	$⊢ ((u \in r \land v \in s) \land ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to (\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s))$
65	60 64	sylanb	$⊢ (⟨u, v⟩ \in (r \times s) \land ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to (\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s))$
66	65	anim1i	$⊢ ((⟨u, v⟩ \in (r \times s) \land ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \land r \times s \subseteq z) \to ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
67	66	anasss	$⊢ (⟨u, v⟩ \in (r \times s) \land (((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land r \times s \subseteq z)) \to ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
68	67	an12s	$⊢ (((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
69	68	expl	$⊢ (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \to (((v \in s \to \exists q \in b (v \in q \land q \subseteq s)) \land (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z))$
70	69	reximdv	$⊢ (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \to (\exists s \in S ((v \in s \to \exists q \in b (v \in q \land q \subseteq s)) \land (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z))$
71	59 70	syl5	$⊢ (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \to ((\forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)) \land \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z))$
72	71	impl	$⊢ (((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
73	72	reximi	$⊢ \exists r \in R (((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists r \in R \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
74	58 73	syl	$⊢ (\forall r \in R ((u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists r \in R \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
75	57 74	sylan	$⊢ ((\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists r \in R \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z)$
76		reeanv	$⊢ \exists p \in a \exists q \in b ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \leftrightarrow (\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s))$
77		simpr1l	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \in a$
78		simpr1r	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to q \in b$
79		eqidd	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \times q = p \times q$
80		xpeq1	$⊢ m = p \to m \times n = p \times n$
81	80	eqeq2d	$⊢ m = p \to (p \times q = m \times n \leftrightarrow p \times q = p \times n)$
82		xpeq2	$⊢ n = q \to p \times n = p \times q$
83	82	eqeq2d	$⊢ n = q \to (p \times q = p \times n \leftrightarrow p \times q = p \times q)$
84	81 83	rspc2ev	$⊢ (p \in a \land q \in b \land p \times q = p \times q) \to \exists m \in a \exists n \in b p \times q = m \times n$
85	77 78 79 84	syl3anc	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to \exists m \in a \exists n \in b p \times q = m \times n$
86		vex	$⊢ p \in V$
87		vex	$⊢ q \in V$
88	86 87	xpex	$⊢ p \times q \in V$
89		eqeq1	$⊢ x = p \times q \to (x = m \times n \leftrightarrow p \times q = m \times n)$
90	89	2rexbidv	$⊢ x = p \times q \to (\exists m \in a \exists n \in b x = m \times n \leftrightarrow \exists m \in a \exists n \in b p \times q = m \times n)$
91	88 90	elab	$⊢ p \times q \in \{x \| \exists m \in a \exists n \in b x = m \times n\} \leftrightarrow \exists m \in a \exists n \in b p \times q = m \times n$
92	85 91	sylibr	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \times q \in \{x \| \exists m \in a \exists n \in b x = m \times n\}$
93	26	rnmpo	$⊢ ran (m \in a, n \in b ⟼ m \times n) = \{x \| \exists m \in a \exists n \in b x = m \times n\}$
94	92 93	eleqtrrdi	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \times q \in ran (m \in a, n \in b ⟼ m \times n)$
95		simpr2	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s))$
96		opelxpi	$⊢ (u \in p \land v \in q) \to ⟨u, v⟩ \in (p \times q)$
97	96	ad2ant2r	$⊢ ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \to ⟨u, v⟩ \in (p \times q)$
98	95 97	syl	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to ⟨u, v⟩ \in (p \times q)$
99		xpss12	$⊢ (p \subseteq r \land q \subseteq s) \to p \times q \subseteq r \times s$
100	99	ad2ant2l	$⊢ ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \to p \times q \subseteq r \times s$
101	95 100	syl	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \times q \subseteq r \times s$
102		simpr3	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to r \times s \subseteq z$
103	101 102	sstrd	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to p \times q \subseteq z$
104		eleq2	$⊢ w = p \times q \to (⟨u, v⟩ \in w \leftrightarrow ⟨u, v⟩ \in (p \times q))$
105		sseq1	$⊢ w = p \times q \to (w \subseteq z \leftrightarrow p \times q \subseteq z)$
106	104 105	anbi12d	$⊢ w = p \times q \to ((⟨u, v⟩ \in w \land w \subseteq z) \leftrightarrow (⟨u, v⟩ \in (p \times q) \land p \times q \subseteq z))$
107	106	rspcev	$⊢ (p \times q \in ran (m \in a, n \in b ⟼ m \times n) \land (⟨u, v⟩ \in (p \times q) \land p \times q \subseteq z)) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)$
108	94 98 103 107	syl12anc	$⊢ ((((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \land ((p \in a \land q \in b) \land ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \land r \times s \subseteq z)) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)$
109	108	3exp2	$⊢ (((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \to ((p \in a \land q \in b) \to (((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \to (r \times s \subseteq z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))))$
110	109	rexlimdvv	$⊢ (((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \to (\exists p \in a \exists q \in b ((u \in p \land p \subseteq r) \land (v \in q \land q \subseteq s)) \to (r \times s \subseteq z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
111	76 110	syl5bir	$⊢ (((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \to ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \to (r \times s \subseteq z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
112	111	impd	$⊢ (((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \land (r \in R \land s \in S)) \to (((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
113	112	rexlimdvva	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \to (\exists r \in R \exists s \in S ((\exists p \in a (u \in p \land p \subseteq r) \land \exists q \in b (v \in q \land q \subseteq s)) \land r \times s \subseteq z) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
114	75 113	syl5	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \to (((\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \land \exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z)) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
115	114	expd	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land (a ≼ ω \land b ≼ ω)) \to ((\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))) \to (\exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
116	115	impr	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to (\exists r \in R \exists s \in S (⟨u, v⟩ \in (r \times s) \land r \times s \subseteq z) \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
117	56 116	syl9r	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to (\forall w \in z \exists r \in R \exists s \in S (w \in (r \times s) \land r \times s \subseteq z) \to (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
118	52 117	sylbid	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to (z \in (R \times_{t} S) \to (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
119	118	ralrimiv	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
120		breq1	$⊢ y = ran (m \in a, n \in b ⟼ m \times n) \to (y ≼ ω \leftrightarrow ran (m \in a, n \in b ⟼ m \times n) ≼ ω)$
121		rexeq	$⊢ y = ran (m \in a, n \in b ⟼ m \times n) \to (\exists w \in y (⟨u, v⟩ \in w \land w \subseteq z) \leftrightarrow \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))$
122	121	imbi2d	$⊢ y = ran (m \in a, n \in b ⟼ m \times n) \to ((⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)) \leftrightarrow (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
123	122	ralbidv	$⊢ y = ran (m \in a, n \in b ⟼ m \times n) \to (\forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)) \leftrightarrow \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))$
124	120 123	anbi12d	$⊢ y = ran (m \in a, n \in b ⟼ m \times n) \to ((y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))) \leftrightarrow (ran (m \in a, n \in b ⟼ m \times n) ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z))))$
125	124	rspcev	$⊢ (ran (m \in a, n \in b ⟼ m \times n) \in 𝒫 (R \times_{t} S) \land (ran (m \in a, n \in b ⟼ m \times n) ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in ran (m \in a, n \in b ⟼ m \times n) (⟨u, v⟩ \in w \land w \subseteq z)))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
126	33 48 119 125	syl12anc	$⊢ ((((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \land ((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s))))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
127	126	ex	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to (((a ≼ ω \land b ≼ ω) \land (\forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r)) \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
128	12 127	syl5bi	$⊢ (((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \land (a \in 𝒫 R \land b \in 𝒫 S)) \to (((a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
129	128	rexlimdvva	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to (\exists a \in 𝒫 R \exists b \in 𝒫 S ((a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
130	11 129	syl5bir	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to ((\exists a \in 𝒫 R (a ≼ ω \land \forall r \in R (u \in r \to \exists p \in a (u \in p \land p \subseteq r))) \land \exists b \in 𝒫 S (b ≼ ω \land \forall s \in S (v \in s \to \exists q \in b (v \in q \land q \subseteq s)))) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
131	7 10 130	mp2and	$⊢ ((R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \land (u \in ⋃ R \land v \in ⋃ S)) \to \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
132	131	ralrimivva	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to \forall u \in ⋃ R \forall v \in ⋃ S \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
133		eleq1	$⊢ x = ⟨u, v⟩ \to (x \in z \leftrightarrow ⟨u, v⟩ \in z)$
134		eleq1	$⊢ x = ⟨u, v⟩ \to (x \in w \leftrightarrow ⟨u, v⟩ \in w)$
135	134	anbi1d	$⊢ x = ⟨u, v⟩ \to ((x \in w \land w \subseteq z) \leftrightarrow (⟨u, v⟩ \in w \land w \subseteq z))$
136	135	rexbidv	$⊢ x = ⟨u, v⟩ \to (\exists w \in y (x \in w \land w \subseteq z) \leftrightarrow \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))$
137	133 136	imbi12d	$⊢ x = ⟨u, v⟩ \to ((x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
138	137	ralbidv	$⊢ x = ⟨u, v⟩ \to (\forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
139	138	anbi2d	$⊢ x = ⟨u, v⟩ \to ((y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
140	139	rexbidv	$⊢ x = ⟨u, v⟩ \to (\exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z))))$
141	140	ralxp	$⊢ \forall x \in (⋃ R \times ⋃ S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow \forall u \in ⋃ R \forall v \in ⋃ S \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (⟨u, v⟩ \in z \to \exists w \in y (⟨u, v⟩ \in w \land w \subseteq z)))$
142	132 141	sylibr	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to \forall x \in (⋃ R \times ⋃ S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
143	5 8	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
144	1 2 143	syl2an	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
145	144	raleqdv	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to (\forall x \in (⋃ R \times ⋃ S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow \forall x \in ⋃ (R \times_{t} S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
146	142 145	mpbid	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to \forall x \in ⋃ (R \times_{t} S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
147		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
148	147	is1stc2	$⊢ R \times_{t} S \in 1^{st} 𝜔 \leftrightarrow (R \times_{t} S \in Top \land \forall x \in ⋃ (R \times_{t} S) \exists y \in 𝒫 (R \times_{t} S) (y ≼ ω \land \forall z \in (R \times_{t} S) (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
149	4 146 148	sylanbrc	$⊢ (R \in 1^{st} 𝜔 \land S \in 1^{st} 𝜔) \to R \times_{t} S \in 1^{st} 𝜔$

Metamath Proof Explorer

Theorem tx1stc

Proof