# Metamath Proof Explorer

## Theorem txindis

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

Ref Expression
Assertion txindis ${⊢}\left\{\varnothing ,{A}\right\}{×}_{t}\left\{\varnothing ,{B}\right\}=\left\{\varnothing ,{A}×{B}\right\}$

### Proof

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