hmphindis

Description: Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Hypothesis	hmphdis.1	$⊢ X = ⋃ J$
	Assertion	hmphindis	$⊢ J ≃ \{\emptyset, A\} \to J = \{\emptyset, X\}$

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	$⊢ X = ⋃ J$
2		dfsn2	$⊢ \{\emptyset\} = \{\emptyset, \emptyset\}$
3		indislem	$⊢ \{\emptyset, I (A)\} = \{\emptyset, A\}$
4		preq2	$⊢ I (A) = \emptyset \to \{\emptyset, I (A)\} = \{\emptyset, \emptyset\}$
5	4 2	eqtr4di	$⊢ I (A) = \emptyset \to \{\emptyset, I (A)\} = \{\emptyset\}$
6	3 5	eqtr3id	$⊢ I (A) = \emptyset \to \{\emptyset, A\} = \{\emptyset\}$
7	6	breq2d	$⊢ I (A) = \emptyset \to (J ≃ \{\emptyset, A\} \leftrightarrow J ≃ \{\emptyset\})$
8	7	biimpac	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to J ≃ \{\emptyset\}$
9		hmph0	$⊢ J ≃ \{\emptyset\} \leftrightarrow J = \{\emptyset\}$
10	8 9	sylib	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to J = \{\emptyset\}$
11	10	unieqd	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to ⋃ J = ⋃ \{\emptyset\}$
12		0ex	$⊢ \emptyset \in V$
13	12	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
14	13	eqcomi	$⊢ \emptyset = ⋃ \{\emptyset\}$
15	11 1 14	3eqtr4g	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to X = \emptyset$
16	15	preq2d	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to \{\emptyset, X\} = \{\emptyset, \emptyset\}$
17	2 10 16	3eqtr4a	$⊢ (J ≃ \{\emptyset, A\} \land I (A) = \emptyset) \to J = \{\emptyset, X\}$
18		hmphen	$⊢ J ≃ \{\emptyset, A\} \to J \approx \{\emptyset, A\}$
19		necom	$⊢ I (A) \neq \emptyset \leftrightarrow \emptyset \neq I (A)$
20		fvex	$⊢ I (A) \in V$
21		pr2nelem	$⊢ (\emptyset \in V \land I (A) \in V \land \emptyset \neq I (A)) \to \{\emptyset, I (A)\} \approx 2_{𝑜}$
22	12 20 21	mp3an12	$⊢ \emptyset \neq I (A) \to \{\emptyset, I (A)\} \approx 2_{𝑜}$
23	19 22	sylbi	$⊢ I (A) \neq \emptyset \to \{\emptyset, I (A)\} \approx 2_{𝑜}$
24	23	adantl	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to \{\emptyset, I (A)\} \approx 2_{𝑜}$
25	3 24	eqbrtrrid	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to \{\emptyset, A\} \approx 2_{𝑜}$
26		entr	$⊢ (J \approx \{\emptyset, A\} \land \{\emptyset, A\} \approx 2_{𝑜}) \to J \approx 2_{𝑜}$
27	18 25 26	syl2an2r	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to J \approx 2_{𝑜}$
28		hmphtop1	$⊢ J ≃ \{\emptyset, A\} \to J \in Top$
29	28	adantr	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to J \in Top$
30	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
31	29 30	sylib	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to J \in TopOn (X)$
32		en2top	$⊢ J \in TopOn (X) \to (J \approx 2_{𝑜} \leftrightarrow (J = \{\emptyset, X\} \land X \neq \emptyset))$
33	31 32	syl	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to (J \approx 2_{𝑜} \leftrightarrow (J = \{\emptyset, X\} \land X \neq \emptyset))$
34	27 33	mpbid	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to (J = \{\emptyset, X\} \land X \neq \emptyset)$
35	34	simpld	$⊢ (J ≃ \{\emptyset, A\} \land I (A) \neq \emptyset) \to J = \{\emptyset, X\}$
36	17 35	pm2.61dane	$⊢ J ≃ \{\emptyset, A\} \to J = \{\emptyset, X\}$

Metamath Proof Explorer

Theorem hmphindis

Proof