This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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