tx2ndc

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

		Ref	Expression
	Assertion	tx2ndc	$⊢ (R \in 2^{nd} 𝜔 \land S \in 2^{nd} 𝜔) \to R \times_{t} S \in 2^{nd} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ R \in 2^{nd} 𝜔 \leftrightarrow \exists r \in TopBases (r ≼ ω \land topGen (r) = R)$
2		is2ndc	$⊢ S \in 2^{nd} 𝜔 \leftrightarrow \exists s \in TopBases (s ≼ ω \land topGen (s) = S)$
3		reeanv	$⊢ \exists r \in TopBases \exists s \in TopBases ((r ≼ ω \land topGen (r) = R) \land (s ≼ ω \land topGen (s) = S)) \leftrightarrow (\exists r \in TopBases (r ≼ ω \land topGen (r) = R) \land \exists s \in TopBases (s ≼ ω \land topGen (s) = S))$
4		an4	$⊢ ((r ≼ ω \land topGen (r) = R) \land (s ≼ ω \land topGen (s) = S)) \leftrightarrow ((r ≼ ω \land s ≼ ω) \land (topGen (r) = R \land topGen (s) = S))$
5		txbasval	$⊢ (r \in TopBases \land s \in TopBases) \to topGen (r) \times_{t} topGen (s) = r \times_{t} s$
6		eqid	$⊢ ran (x \in r, y \in s ⟼ x \times y) = ran (x \in r, y \in s ⟼ x \times y)$
7	6	txval	$⊢ (r \in TopBases \land s \in TopBases) \to r \times_{t} s = topGen (ran (x \in r, y \in s ⟼ x \times y))$
8	5 7	eqtrd	$⊢ (r \in TopBases \land s \in TopBases) \to topGen (r) \times_{t} topGen (s) = topGen (ran (x \in r, y \in s ⟼ x \times y))$
9	8	adantr	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to topGen (r) \times_{t} topGen (s) = topGen (ran (x \in r, y \in s ⟼ x \times y))$
10	6	txbas	$⊢ (r \in TopBases \land s \in TopBases) \to ran (x \in r, y \in s ⟼ x \times y) \in TopBases$
11	10	adantr	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to ran (x \in r, y \in s ⟼ x \times y) \in TopBases$
12		omelon	$⊢ ω \in On$
13		vex	$⊢ s \in V$
14	13	xpdom1	$⊢ r ≼ ω \to (r \times s) ≼ (ω \times s)$
15		omex	$⊢ ω \in V$
16	15	xpdom2	$⊢ s ≼ ω \to (ω \times s) ≼ (ω \times ω)$
17		domtr	$⊢ ((r \times s) ≼ (ω \times s) \land (ω \times s) ≼ (ω \times ω)) \to (r \times s) ≼ (ω \times ω)$
18	14 16 17	syl2an	$⊢ (r ≼ ω \land s ≼ ω) \to (r \times s) ≼ (ω \times ω)$
19	18	adantl	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to (r \times s) ≼ (ω \times ω)$
20		xpomen	$⊢ (ω \times ω) \approx ω$
21		domentr	$⊢ ((r \times s) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (r \times s) ≼ ω$
22	19 20 21	sylancl	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to (r \times s) ≼ ω$
23		ondomen	$⊢ (ω \in On \land (r \times s) ≼ ω) \to r \times s \in dom card$
24	12 22 23	sylancr	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to r \times s \in dom card$
25		eqid	$⊢ (x \in r, y \in s ⟼ x \times y) = (x \in r, y \in s ⟼ x \times y)$
26		vex	$⊢ x \in V$
27		vex	$⊢ y \in V$
28	26 27	xpex	$⊢ x \times y \in V$
29	25 28	fnmpoi	$⊢ (x \in r, y \in s ⟼ x \times y) Fn (r \times s)$
30	29	a1i	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to (x \in r, y \in s ⟼ x \times y) Fn (r \times s)$
31		dffn4	$⊢ (x \in r, y \in s ⟼ x \times y) Fn (r \times s) \leftrightarrow (x \in r, y \in s ⟼ x \times y) : r \times s \underset{onto}{⟶} ran (x \in r, y \in s ⟼ x \times y)$
32	30 31	sylib	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to (x \in r, y \in s ⟼ x \times y) : r \times s \underset{onto}{⟶} ran (x \in r, y \in s ⟼ x \times y)$
33		fodomnum	$⊢ r \times s \in dom card \to ((x \in r, y \in s ⟼ x \times y) : r \times s \underset{onto}{⟶} ran (x \in r, y \in s ⟼ x \times y) \to ran (x \in r, y \in s ⟼ x \times y) ≼ (r \times s))$
34	24 32 33	sylc	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to ran (x \in r, y \in s ⟼ x \times y) ≼ (r \times s)$
35		domtr	$⊢ (ran (x \in r, y \in s ⟼ x \times y) ≼ (r \times s) \land (r \times s) ≼ ω) \to ran (x \in r, y \in s ⟼ x \times y) ≼ ω$
36	34 22 35	syl2anc	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to ran (x \in r, y \in s ⟼ x \times y) ≼ ω$
37		2ndci	$⊢ (ran (x \in r, y \in s ⟼ x \times y) \in TopBases \land ran (x \in r, y \in s ⟼ x \times y) ≼ ω) \to topGen (ran (x \in r, y \in s ⟼ x \times y)) \in 2^{nd} 𝜔$
38	11 36 37	syl2anc	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to topGen (ran (x \in r, y \in s ⟼ x \times y)) \in 2^{nd} 𝜔$
39	9 38	eqeltrd	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to topGen (r) \times_{t} topGen (s) \in 2^{nd} 𝜔$
40		oveq12	$⊢ (topGen (r) = R \land topGen (s) = S) \to topGen (r) \times_{t} topGen (s) = R \times_{t} S$
41	40	eleq1d	$⊢ (topGen (r) = R \land topGen (s) = S) \to (topGen (r) \times_{t} topGen (s) \in 2^{nd} 𝜔 \leftrightarrow R \times_{t} S \in 2^{nd} 𝜔)$
42	39 41	syl5ibcom	$⊢ ((r \in TopBases \land s \in TopBases) \land (r ≼ ω \land s ≼ ω)) \to ((topGen (r) = R \land topGen (s) = S) \to R \times_{t} S \in 2^{nd} 𝜔)$
43	42	expimpd	$⊢ (r \in TopBases \land s \in TopBases) \to (((r ≼ ω \land s ≼ ω) \land (topGen (r) = R \land topGen (s) = S)) \to R \times_{t} S \in 2^{nd} 𝜔)$
44	4 43	biimtrid	$⊢ (r \in TopBases \land s \in TopBases) \to (((r ≼ ω \land topGen (r) = R) \land (s ≼ ω \land topGen (s) = S)) \to R \times_{t} S \in 2^{nd} 𝜔)$
45	44	rexlimivv	$⊢ \exists r \in TopBases \exists s \in TopBases ((r ≼ ω \land topGen (r) = R) \land (s ≼ ω \land topGen (s) = S)) \to R \times_{t} S \in 2^{nd} 𝜔$
46	3 45	sylbir	$⊢ (\exists r \in TopBases (r ≼ ω \land topGen (r) = R) \land \exists s \in TopBases (s ≼ ω \land topGen (s) = S)) \to R \times_{t} S \in 2^{nd} 𝜔$
47	1 2 46	syl2anb	$⊢ (R \in 2^{nd} 𝜔 \land S \in 2^{nd} 𝜔) \to R \times_{t} S \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem tx2ndc

Proof