txdis

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

		Ref	Expression
	Assertion	txdis	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) = 𝒫 ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		distop	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2		distop	⊢ ( 𝐵 ∈ 𝑊 → 𝒫 𝐵 ∈ Top )
3		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
4	3	eqcomi	⊢ 𝐴 = ∪ 𝒫 𝐴
5		unipw	⊢ ∪ 𝒫 𝐵 = 𝐵
6	5	eqcomi	⊢ 𝐵 = ∪ 𝒫 𝐵
7	4 6	txuni	⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) )
8	1 2 7	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) )
9		eqimss2	⊢ ( ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) → ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
11		sspwuni	⊢ ( ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) ↔ ∪ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
12	10 11	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) )
13		elelpwi	⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) )
14	13	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) )
15		xp1st	⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ 𝑦 ) ∈ 𝐴 )
16		snelpwi	⊢ ( ( 1^st ‘ 𝑦 ) ∈ 𝐴 → { ( 1^st ‘ 𝑦 ) } ∈ 𝒫 𝐴 )
17	14 15 16	3syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 1^st ‘ 𝑦 ) } ∈ 𝒫 𝐴 )
18		xp2nd	⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ 𝑦 ) ∈ 𝐵 )
19		snelpwi	⊢ ( ( 2^nd ‘ 𝑦 ) ∈ 𝐵 → { ( 2^nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 )
20	14 18 19	3syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 2^nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 )
21		vsnid	⊢ 𝑦 ∈ { 𝑦 }
22		1st2nd2	⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
23	14 22	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
24	23	sneqd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { 𝑦 } = { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
25	21 24	eleqtrid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
26		simprl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ 𝑥 )
27	23 26	eqeltrrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ 𝑥 )
28	27	snssd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ⊆ 𝑥 )
29		xpeq1	⊢ ( 𝑧 = { ( 1^st ‘ 𝑦 ) } → ( 𝑧 × 𝑤 ) = ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) )
30	29	eleq2d	⊢ ( 𝑧 = { ( 1^st ‘ 𝑦 ) } → ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ↔ 𝑦 ∈ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ) )
31	29	sseq1d	⊢ ( 𝑧 = { ( 1^st ‘ 𝑦 ) } → ( ( 𝑧 × 𝑤 ) ⊆ 𝑥 ↔ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) )
32	30 31	anbi12d	⊢ ( 𝑧 = { ( 1^st ‘ 𝑦 ) } → ( ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ∧ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ) )
33		xpeq2	⊢ ( 𝑤 = { ( 2^nd ‘ 𝑦 ) } → ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) = ( { ( 1^st ‘ 𝑦 ) } × { ( 2^nd ‘ 𝑦 ) } ) )
34		fvex	⊢ ( 1^st ‘ 𝑦 ) ∈ V
35		fvex	⊢ ( 2^nd ‘ 𝑦 ) ∈ V
36	34 35	xpsn	⊢ ( { ( 1^st ‘ 𝑦 ) } × { ( 2^nd ‘ 𝑦 ) } ) = { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ }
37	33 36	eqtrdi	⊢ ( 𝑤 = { ( 2^nd ‘ 𝑦 ) } → ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) = { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
38	37	eleq2d	⊢ ( 𝑤 = { ( 2^nd ‘ 𝑦 ) } → ( 𝑦 ∈ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ↔ 𝑦 ∈ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ) )
39	37	sseq1d	⊢ ( 𝑤 = { ( 2^nd ‘ 𝑦 ) } → ( ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ↔ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ⊆ 𝑥 ) )
40	38 39	anbi12d	⊢ ( 𝑤 = { ( 2^nd ‘ 𝑦 ) } → ( ( 𝑦 ∈ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ∧ ( { ( 1^st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ∧ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ⊆ 𝑥 ) ) )
41	32 40	rspc2ev	⊢ ( ( { ( 1^st ‘ 𝑦 ) } ∈ 𝒫 𝐴 ∧ { ( 2^nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 ∧ ( 𝑦 ∈ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ∧ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) )
42	17 20 25 28 41	syl112anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) )
43	42	expr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
44	43	ralrimdva	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
45		eltx	⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
46	1 2 45	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
47	44 46	sylibrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → 𝑥 ∈ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) ) )
48	47	ssrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ⊆ ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) )
49	12 48	eqssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 ×_t 𝒫 𝐵 ) = 𝒫 ( 𝐴 × 𝐵 ) )

Metamath Proof Explorer

Theorem txdis

Proof