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	⊢ 𝑋 = ∪ 𝐽
Assertion	hmphindis	⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 = { ∅ , 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		hmphdis.1	⊢ 𝑋 = ∪ 𝐽
2		dfsn2	⊢ { ∅ } = { ∅ , ∅ }
3		indislem	⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }
4		preq2	⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , ( I ‘ 𝐴 ) } = { ∅ , ∅ } )
5	4 2	eqtr4di	⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , ( I ‘ 𝐴 ) } = { ∅ } )
6	3 5	eqtr3id	⊢ ( ( I ‘ 𝐴 ) = ∅ → { ∅ , 𝐴 } = { ∅ } )
7	6	breq2d	⊢ ( ( I ‘ 𝐴 ) = ∅ → ( 𝐽 ≃ { ∅ , 𝐴 } ↔ 𝐽 ≃ { ∅ } ) )
8	7	biimpac	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 ≃ { ∅ } )
9		hmph0	⊢ ( 𝐽 ≃ { ∅ } ↔ 𝐽 = { ∅ } )
10	8 9	sylib	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 = { ∅ } )
11	10	unieqd	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → ∪ 𝐽 = ∪ { ∅ } )
12		0ex	⊢ ∅ ∈ V
13	12	unisn	⊢ ∪ { ∅ } = ∅
14	13	eqcomi	⊢ ∅ = ∪ { ∅ }
15	11 1 14	3eqtr4g	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝑋 = ∅ )
16	15	preq2d	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → { ∅ , 𝑋 } = { ∅ , ∅ } )
17	2 10 16	3eqtr4a	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) = ∅ ) → 𝐽 = { ∅ , 𝑋 } )
18		hmphen	⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 ≈ { ∅ , 𝐴 } )
19		necom	⊢ ( ( I ‘ 𝐴 ) ≠ ∅ ↔ ∅ ≠ ( I ‘ 𝐴 ) )
20		fvex	⊢ ( I ‘ 𝐴 ) ∈ V
21		pr2nelem	⊢ ( ( ∅ ∈ V ∧ ( I ‘ 𝐴 ) ∈ V ∧ ∅ ≠ ( I ‘ 𝐴 ) ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o )
22	12 20 21	mp3an12	⊢ ( ∅ ≠ ( I ‘ 𝐴 ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o )
23	19 22	sylbi	⊢ ( ( I ‘ 𝐴 ) ≠ ∅ → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o )
24	23	adantl	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → { ∅ , ( I ‘ 𝐴 ) } ≈ 2o )
25	3 24	eqbrtrrid	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → { ∅ , 𝐴 } ≈ 2o )
26		entr	⊢ ( ( 𝐽 ≈ { ∅ , 𝐴 } ∧ { ∅ , 𝐴 } ≈ 2o ) → 𝐽 ≈ 2o )
27	18 25 26	syl2an2r	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ≈ 2o )
28		hmphtop1	⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 ∈ Top )
29	28	adantr	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ∈ Top )
30	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
31	29 30	sylib	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
32		en2top	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) )
33	31 32	syl	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) )
34	27 33	mpbid	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) )
35	34	simpld	⊢ ( ( 𝐽 ≃ { ∅ , 𝐴 } ∧ ( I ‘ 𝐴 ) ≠ ∅ ) → 𝐽 = { ∅ , 𝑋 } )
36	17 35	pm2.61dane	⊢ ( 𝐽 ≃ { ∅ , 𝐴 } → 𝐽 = { ∅ , 𝑋 } )