txindis

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

		Ref	Expression
	Assertion	txindis	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} = \{\emptyset, A \times B\}$

Proof

Step	Hyp	Ref	Expression
1		neq0	$⊢ \neg x = \emptyset \leftrightarrow \exists y y \in x$
2		indistop	$⊢ \{\emptyset, A\} \in Top$
3		indistop	$⊢ \{\emptyset, B\} \in Top$
4		eltx	$⊢ (\{\emptyset, A\} \in Top \land \{\emptyset, B\} \in Top) \to (x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \leftrightarrow \forall y \in x \exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x))$
5	2 3 4	mp2an	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \leftrightarrow \forall y \in x \exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x)$
6		rsp	$⊢ \forall y \in x \exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x) \to (y \in x \to \exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x))$
7	5 6	sylbi	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (y \in x \to \exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x))$
8		elssuni	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to x \subseteq ⋃ (\{\emptyset, A\} \times_{t} \{\emptyset, B\})$
9		indisuni	$⊢ I (A) = ⋃ \{\emptyset, A\}$
10		indisuni	$⊢ I (B) = ⋃ \{\emptyset, B\}$
11	2 3 9 10	txunii	$⊢ I (A) \times I (B) = ⋃ (\{\emptyset, A\} \times_{t} \{\emptyset, B\})$
12	8 11	sseqtrrdi	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to x \subseteq I (A) \times I (B)$
13	12	ad2antrr	$⊢ ((x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \land (z \in \{\emptyset, A\} \land w \in \{\emptyset, B\})) \land (y \in (z \times w) \land z \times w \subseteq x)) \to x \subseteq I (A) \times I (B)$
14		ne0i	$⊢ y \in (z \times w) \to z \times w \neq \emptyset$
15	14	ad2antrl	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \times w \neq \emptyset$
16		xpnz	$⊢ (z \neq \emptyset \land w \neq \emptyset) \leftrightarrow z \times w \neq \emptyset$
17	15 16	sylibr	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to (z \neq \emptyset \land w \neq \emptyset)$
18	17	simpld	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \neq \emptyset$
19	18	neneqd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to \neg z = \emptyset$
20		simpll	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \in \{\emptyset, A\}$
21		indislem	$⊢ \{\emptyset, I (A)\} = \{\emptyset, A\}$
22	20 21	eleqtrrdi	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \in \{\emptyset, I (A)\}$
23		elpri	$⊢ z \in \{\emptyset, I (A)\} \to (z = \emptyset \lor z = I (A))$
24	22 23	syl	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to (z = \emptyset \lor z = I (A))$
25	24	ord	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to (\neg z = \emptyset \to z = I (A))$
26	19 25	mpd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z = I (A)$
27	17	simprd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to w \neq \emptyset$
28	27	neneqd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to \neg w = \emptyset$
29		simplr	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to w \in \{\emptyset, B\}$
30		indislem	$⊢ \{\emptyset, I (B)\} = \{\emptyset, B\}$
31	29 30	eleqtrrdi	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to w \in \{\emptyset, I (B)\}$
32		elpri	$⊢ w \in \{\emptyset, I (B)\} \to (w = \emptyset \lor w = I (B))$
33	31 32	syl	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to (w = \emptyset \lor w = I (B))$
34	33	ord	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to (\neg w = \emptyset \to w = I (B))$
35	28 34	mpd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to w = I (B)$
36	26 35	xpeq12d	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \times w = I (A) \times I (B)$
37		simprr	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to z \times w \subseteq x$
38	36 37	eqsstrrd	$⊢ ((z \in \{\emptyset, A\} \land w \in \{\emptyset, B\}) \land (y \in (z \times w) \land z \times w \subseteq x)) \to I (A) \times I (B) \subseteq x$
39	38	adantll	$⊢ ((x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \land (z \in \{\emptyset, A\} \land w \in \{\emptyset, B\})) \land (y \in (z \times w) \land z \times w \subseteq x)) \to I (A) \times I (B) \subseteq x$
40	13 39	eqssd	$⊢ ((x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \land (z \in \{\emptyset, A\} \land w \in \{\emptyset, B\})) \land (y \in (z \times w) \land z \times w \subseteq x)) \to x = I (A) \times I (B)$
41	40	ex	$⊢ (x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \land (z \in \{\emptyset, A\} \land w \in \{\emptyset, B\})) \to ((y \in (z \times w) \land z \times w \subseteq x) \to x = I (A) \times I (B))$
42	41	rexlimdvva	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (\exists z \in \{\emptyset, A\} \exists w \in \{\emptyset, B\} (y \in (z \times w) \land z \times w \subseteq x) \to x = I (A) \times I (B))$
43	7 42	syld	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (y \in x \to x = I (A) \times I (B))$
44	43	exlimdv	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (\exists y y \in x \to x = I (A) \times I (B))$
45	1 44	syl5bi	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (\neg x = \emptyset \to x = I (A) \times I (B))$
46	45	orrd	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to (x = \emptyset \lor x = I (A) \times I (B))$
47		vex	$⊢ x \in V$
48	47	elpr	$⊢ x \in \{\emptyset, I (A) \times I (B)\} \leftrightarrow (x = \emptyset \lor x = I (A) \times I (B))$
49	46 48	sylibr	$⊢ x \in (\{\emptyset, A\} \times_{t} \{\emptyset, B\}) \to x \in \{\emptyset, I (A) \times I (B)\}$
50	49	ssriv	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} \subseteq \{\emptyset, I (A) \times I (B)\}$
51	9	toptopon	$⊢ \{\emptyset, A\} \in Top \leftrightarrow \{\emptyset, A\} \in TopOn (I (A))$
52	2 51	mpbi	$⊢ \{\emptyset, A\} \in TopOn (I (A))$
53	10	toptopon	$⊢ \{\emptyset, B\} \in Top \leftrightarrow \{\emptyset, B\} \in TopOn (I (B))$
54	3 53	mpbi	$⊢ \{\emptyset, B\} \in TopOn (I (B))$
55		txtopon	$⊢ (\{\emptyset, A\} \in TopOn (I (A)) \land \{\emptyset, B\} \in TopOn (I (B))) \to \{\emptyset, A\} \times_{t} \{\emptyset, B\} \in TopOn (I (A) \times I (B))$
56	52 54 55	mp2an	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} \in TopOn (I (A) \times I (B))$
57		topgele	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} \in TopOn (I (A) \times I (B)) \to (\{\emptyset, I (A) \times I (B)\} \subseteq \{\emptyset, A\} \times_{t} \{\emptyset, B\} \land \{\emptyset, A\} \times_{t} \{\emptyset, B\} \subseteq 𝒫 (I (A) \times I (B)))$
58	56 57	ax-mp	$⊢ (\{\emptyset, I (A) \times I (B)\} \subseteq \{\emptyset, A\} \times_{t} \{\emptyset, B\} \land \{\emptyset, A\} \times_{t} \{\emptyset, B\} \subseteq 𝒫 (I (A) \times I (B)))$
59	58	simpli	$⊢ \{\emptyset, I (A) \times I (B)\} \subseteq \{\emptyset, A\} \times_{t} \{\emptyset, B\}$
60	50 59	eqssi	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} = \{\emptyset, I (A) \times I (B)\}$
61		txindislem	$⊢ I (A) \times I (B) = I (A \times B)$
62	61	preq2i	$⊢ \{\emptyset, I (A) \times I (B)\} = \{\emptyset, I (A \times B)\}$
63		indislem	$⊢ \{\emptyset, I (A \times B)\} = \{\emptyset, A \times B\}$
64	60 62 63	3eqtri	$⊢ \{\emptyset, A\} \times_{t} \{\emptyset, B\} = \{\emptyset, A \times B\}$

Metamath Proof Explorer

Theorem txindis

Proof