en2top

Description: If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	en2top	$⊢ J \in TopOn (X) \to (J \approx 2_{𝑜} \leftrightarrow (J = \{\emptyset, X\} \land X \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to J \approx 2_{𝑜}$
2		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
3	2	ad2ant2rl	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land (X = \emptyset \land x \in J)) \to x \subseteq X$
4		simprl	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land (X = \emptyset \land x \in J)) \to X = \emptyset$
5		sseq0	$⊢ (x \subseteq X \land X = \emptyset) \to x = \emptyset$
6	3 4 5	syl2anc	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land (X = \emptyset \land x \in J)) \to x = \emptyset$
7		velsn	$⊢ x \in \{\emptyset\} \leftrightarrow x = \emptyset$
8	6 7	sylibr	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land (X = \emptyset \land x \in J)) \to x \in \{\emptyset\}$
9	8	expr	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to (x \in J \to x \in \{\emptyset\})$
10	9	ssrdv	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to J \subseteq \{\emptyset\}$
11		topontop	$⊢ J \in TopOn (X) \to J \in Top$
12		0opn	$⊢ J \in Top \to \emptyset \in J$
13	11 12	syl	$⊢ J \in TopOn (X) \to \emptyset \in J$
14	13	ad2antrr	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to \emptyset \in J$
15	14	snssd	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to \{\emptyset\} \subseteq J$
16	10 15	eqssd	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to J = \{\emptyset\}$
17		0ex	$⊢ \emptyset \in V$
18	17	ensn1	$⊢ \{\emptyset\} \approx 1_{𝑜}$
19	16 18	eqbrtrdi	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to J \approx 1_{𝑜}$
20	19	olcd	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to (J = \emptyset \lor J \approx 1_{𝑜})$
21		sdom2en01	$⊢ J ≺ 2_{𝑜} \leftrightarrow (J = \emptyset \lor J \approx 1_{𝑜})$
22	20 21	sylibr	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to J ≺ 2_{𝑜}$
23		sdomnen	$⊢ J ≺ 2_{𝑜} \to \neg J \approx 2_{𝑜}$
24	22 23	syl	$⊢ ((J \in TopOn (X) \land J \approx 2_{𝑜}) \land X = \emptyset) \to \neg J \approx 2_{𝑜}$
25	24	ex	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to (X = \emptyset \to \neg J \approx 2_{𝑜})$
26	25	necon2ad	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to (J \approx 2_{𝑜} \to X \neq \emptyset)$
27	1 26	mpd	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to X \neq \emptyset$
28	27	necomd	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to \emptyset \neq X$
29	13	adantr	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to \emptyset \in J$
30		toponmax	$⊢ J \in TopOn (X) \to X \in J$
31	30	adantr	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to X \in J$
32		en2eqpr	$⊢ (J \approx 2_{𝑜} \land \emptyset \in J \land X \in J) \to (\emptyset \neq X \to J = \{\emptyset, X\})$
33	1 29 31 32	syl3anc	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to (\emptyset \neq X \to J = \{\emptyset, X\})$
34	28 33	mpd	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to J = \{\emptyset, X\}$
35	34 27	jca	$⊢ (J \in TopOn (X) \land J \approx 2_{𝑜}) \to (J = \{\emptyset, X\} \land X \neq \emptyset)$
36		simprl	$⊢ (J \in TopOn (X) \land (J = \{\emptyset, X\} \land X \neq \emptyset)) \to J = \{\emptyset, X\}$
37		simprr	$⊢ (J \in TopOn (X) \land (J = \{\emptyset, X\} \land X \neq \emptyset)) \to X \neq \emptyset$
38	37	necomd	$⊢ (J \in TopOn (X) \land (J = \{\emptyset, X\} \land X \neq \emptyset)) \to \emptyset \neq X$
39		enpr2	$⊢ (\emptyset \in V \land X \in J \land \emptyset \neq X) \to \{\emptyset, X\} \approx 2_{𝑜}$
40	17 30 38 39	mp3an2ani	$⊢ (J \in TopOn (X) \land (J = \{\emptyset, X\} \land X \neq \emptyset)) \to \{\emptyset, X\} \approx 2_{𝑜}$
41	36 40	eqbrtrd	$⊢ (J \in TopOn (X) \land (J = \{\emptyset, X\} \land X \neq \emptyset)) \to J \approx 2_{𝑜}$
42	35 41	impbida	$⊢ J \in TopOn (X) \to (J \approx 2_{𝑜} \leftrightarrow (J = \{\emptyset, X\} \land X \neq \emptyset))$

Metamath Proof Explorer

Theorem en2top

Proof