Theorem 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 = U. J
Assertion	hmphindis	|- ( J ~= { (/) , A } -> J = { (/) , X } )

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	|- X = U. J
2		dfsn2	|- { (/) } = { (/) , (/) }
3		indislem	|- { (/) , ( _I ` A ) } = { (/) , A }
4		preq2	|- ( ( _I ` A ) = (/) -> { (/) , ( _I ` A ) } = { (/) , (/) } )
5	4 2	eqtr4di	|- ( ( _I ` A ) = (/) -> { (/) , ( _I ` A ) } = { (/) } )
6	3 5	eqtr3id	|- ( ( _I ` A ) = (/) -> { (/) , A } = { (/) } )
7	6	breq2d	|- ( ( _I ` A ) = (/) -> ( J ~= { (/) , A } <-> J ~= { (/) } ) )
8	7	biimpac	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J ~= { (/) } )
9		hmph0	|- ( J ~= { (/) } <-> J = { (/) } )
10	8 9	sylib	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J = { (/) } )
11	10	unieqd	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> U. J = U. { (/) } )
12		0ex	|- (/) e. _V
13	12	unisn	|- U. { (/) } = (/)
14	13	eqcomi	|- (/) = U. { (/) }
15	11 1 14	3eqtr4g	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> X = (/) )
16	15	preq2d	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> { (/) , X } = { (/) , (/) } )
17	2 10 16	3eqtr4a	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) = (/) ) -> J = { (/) , X } )
18		hmphen	|- ( J ~= { (/) , A } -> J ~~ { (/) , A } )
19		necom	|- ( ( _I ` A ) =/= (/) <-> (/) =/= ( _I ` A ) )
20		fvex	|- ( _I ` A ) e. _V
21		enpr2	|- ( ( (/) e. _V /\ ( _I ` A ) e. _V /\ (/) =/= ( _I ` A ) ) -> { (/) , ( _I ` A ) } ~~ 2o )
22	12 20 21	mp3an12	|- ( (/) =/= ( _I ` A ) -> { (/) , ( _I ` A ) } ~~ 2o )
23	19 22	sylbi	|- ( ( _I ` A ) =/= (/) -> { (/) , ( _I ` A ) } ~~ 2o )
24	23	adantl	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> { (/) , ( _I ` A ) } ~~ 2o )
25	3 24	eqbrtrrid	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> { (/) , A } ~~ 2o )
26		entr	|- ( ( J ~~ { (/) , A } /\ { (/) , A } ~~ 2o ) -> J ~~ 2o )
27	18 25 26	syl2an2r	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J ~~ 2o )
28		hmphtop1	|- ( J ~= { (/) , A } -> J e. Top )
29	28	adantr	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J e. Top )
30	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
31	29 30	sylib	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J e. ( TopOn ` X ) )
32		en2top	|- ( J e. ( TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )
33	31 32	syl	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )
34	27 33	mpbid	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> ( J = { (/) , X } /\ X =/= (/) ) )
35	34	simpld	|- ( ( J ~= { (/) , A } /\ ( _I ` A ) =/= (/) ) -> J = { (/) , X } )
36	17 35	pm2.61dane	|- ( J ~= { (/) , A } -> J = { (/) , X } )