txdis

Description: The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	txdis	$⊢ (A \in V \land B \in W) \to 𝒫 A \times_{t} 𝒫 B = 𝒫 (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		distop	$⊢ A \in V \to 𝒫 A \in Top$
2		distop	$⊢ B \in W \to 𝒫 B \in Top$
3		unipw	$⊢ ⋃ 𝒫 A = A$
4	3	eqcomi	$⊢ A = ⋃ 𝒫 A$
5		unipw	$⊢ ⋃ 𝒫 B = B$
6	5	eqcomi	$⊢ B = ⋃ 𝒫 B$
7	4 6	txuni	$⊢ (𝒫 A \in Top \land 𝒫 B \in Top) \to A \times B = ⋃ (𝒫 A \times_{t} 𝒫 B)$
8	1 2 7	syl2an	$⊢ (A \in V \land B \in W) \to A \times B = ⋃ (𝒫 A \times_{t} 𝒫 B)$
9		eqimss2	$⊢ A \times B = ⋃ (𝒫 A \times_{t} 𝒫 B) \to ⋃ (𝒫 A \times_{t} 𝒫 B) \subseteq A \times B$
10	8 9	syl	$⊢ (A \in V \land B \in W) \to ⋃ (𝒫 A \times_{t} 𝒫 B) \subseteq A \times B$
11		sspwuni	$⊢ 𝒫 A \times_{t} 𝒫 B \subseteq 𝒫 (A \times B) \leftrightarrow ⋃ (𝒫 A \times_{t} 𝒫 B) \subseteq A \times B$
12	10 11	sylibr	$⊢ (A \in V \land B \in W) \to 𝒫 A \times_{t} 𝒫 B \subseteq 𝒫 (A \times B)$
13		elelpwi	$⊢ (y \in x \land x \in 𝒫 (A \times B)) \to y \in (A \times B)$
14	13	adantl	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to y \in (A \times B)$
15		xp1st	$⊢ y \in (A \times B) \to 1^{st} (y) \in A$
16		snelpwi	$⊢ 1^{st} (y) \in A \to \{1^{st} (y)\} \in 𝒫 A$
17	14 15 16	3syl	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to \{1^{st} (y)\} \in 𝒫 A$
18		xp2nd	$⊢ y \in (A \times B) \to 2^{nd} (y) \in B$
19		snelpwi	$⊢ 2^{nd} (y) \in B \to \{2^{nd} (y)\} \in 𝒫 B$
20	14 18 19	3syl	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to \{2^{nd} (y)\} \in 𝒫 B$
21		vsnid	$⊢ y \in \{y\}$
22		1st2nd2	$⊢ y \in (A \times B) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
23	14 22	syl	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
24	23	sneqd	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to \{y\} = \{⟨1^{st} (y), 2^{nd} (y)⟩\}$
25	21 24	eleqtrid	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to y \in \{⟨1^{st} (y), 2^{nd} (y)⟩\}$
26		simprl	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to y \in x$
27	23 26	eqeltrrd	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to ⟨1^{st} (y), 2^{nd} (y)⟩ \in x$
28	27	snssd	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to \{⟨1^{st} (y), 2^{nd} (y)⟩\} \subseteq x$
29		xpeq1	$⊢ z = \{1^{st} (y)\} \to z \times w = \{1^{st} (y)\} \times w$
30	29	eleq2d	$⊢ z = \{1^{st} (y)\} \to (y \in (z \times w) \leftrightarrow y \in (\{1^{st} (y)\} \times w))$
31	29	sseq1d	$⊢ z = \{1^{st} (y)\} \to (z \times w \subseteq x \leftrightarrow \{1^{st} (y)\} \times w \subseteq x)$
32	30 31	anbi12d	$⊢ z = \{1^{st} (y)\} \to ((y \in (z \times w) \land z \times w \subseteq x) \leftrightarrow (y \in (\{1^{st} (y)\} \times w) \land \{1^{st} (y)\} \times w \subseteq x))$
33		xpeq2	$⊢ w = \{2^{nd} (y)\} \to \{1^{st} (y)\} \times w = \{1^{st} (y)\} \times \{2^{nd} (y)\}$
34		fvex	$⊢ 1^{st} (y) \in V$
35		fvex	$⊢ 2^{nd} (y) \in V$
36	34 35	xpsn	$⊢ \{1^{st} (y)\} \times \{2^{nd} (y)\} = \{⟨1^{st} (y), 2^{nd} (y)⟩\}$
37	33 36	eqtrdi	$⊢ w = \{2^{nd} (y)\} \to \{1^{st} (y)\} \times w = \{⟨1^{st} (y), 2^{nd} (y)⟩\}$
38	37	eleq2d	$⊢ w = \{2^{nd} (y)\} \to (y \in (\{1^{st} (y)\} \times w) \leftrightarrow y \in \{⟨1^{st} (y), 2^{nd} (y)⟩\})$
39	37	sseq1d	$⊢ w = \{2^{nd} (y)\} \to (\{1^{st} (y)\} \times w \subseteq x \leftrightarrow \{⟨1^{st} (y), 2^{nd} (y)⟩\} \subseteq x)$
40	38 39	anbi12d	$⊢ w = \{2^{nd} (y)\} \to ((y \in (\{1^{st} (y)\} \times w) \land \{1^{st} (y)\} \times w \subseteq x) \leftrightarrow (y \in \{⟨1^{st} (y), 2^{nd} (y)⟩\} \land \{⟨1^{st} (y), 2^{nd} (y)⟩\} \subseteq x))$
41	32 40	rspc2ev	$⊢ (\{1^{st} (y)\} \in 𝒫 A \land \{2^{nd} (y)\} \in 𝒫 B \land (y \in \{⟨1^{st} (y), 2^{nd} (y)⟩\} \land \{⟨1^{st} (y), 2^{nd} (y)⟩\} \subseteq x)) \to \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x)$
42	17 20 25 28 41	syl112anc	$⊢ ((A \in V \land B \in W) \land (y \in x \land x \in 𝒫 (A \times B))) \to \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x)$
43	42	expr	$⊢ ((A \in V \land B \in W) \land y \in x) \to (x \in 𝒫 (A \times B) \to \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x))$
44	43	ralrimdva	$⊢ (A \in V \land B \in W) \to (x \in 𝒫 (A \times B) \to \forall y \in x \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x))$
45		eltx	$⊢ (𝒫 A \in Top \land 𝒫 B \in Top) \to (x \in (𝒫 A \times_{t} 𝒫 B) \leftrightarrow \forall y \in x \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x))$
46	1 2 45	syl2an	$⊢ (A \in V \land B \in W) \to (x \in (𝒫 A \times_{t} 𝒫 B) \leftrightarrow \forall y \in x \exists z \in 𝒫 A \exists w \in 𝒫 B (y \in (z \times w) \land z \times w \subseteq x))$
47	44 46	sylibrd	$⊢ (A \in V \land B \in W) \to (x \in 𝒫 (A \times B) \to x \in (𝒫 A \times_{t} 𝒫 B))$
48	47	ssrdv	$⊢ (A \in V \land B \in W) \to 𝒫 (A \times B) \subseteq 𝒫 A \times_{t} 𝒫 B$
49	12 48	eqssd	$⊢ (A \in V \land B \in W) \to 𝒫 A \times_{t} 𝒫 B = 𝒫 (A \times B)$

Metamath Proof Explorer

Theorem txdis

Proof