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

Metamath Proof Explorer

Theorem restsn

Description: The only subspace topology induced by the topology { (/) } . (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion restsn ( 𝐴 ∈ 𝑉 → ( { ∅ } ↾t 𝐴 ) = { ∅ } )

Proof

Step Hyp Ref Expression
1 sn0top ⊢ { ∅ } ∈ Top
2 elrest ⊢ ( ( { ∅ } ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( { ∅ } ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ { ∅ } 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( { ∅ } ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ { ∅ } 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
4 0ex ⊢ ∅ ∈ V
5 ineq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∩ 𝐴 ) = ( ∅ ∩ 𝐴 ) )
6 0in ⊢ ( ∅ ∩ 𝐴 ) = ∅
7 5 6 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑦 ∩ 𝐴 ) = ∅ )
8 7 eqeq2d ⊢ ( 𝑦 = ∅ → ( 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑥 = ∅ ) )
9 4 8 rexsn ⊢ ( ∃ 𝑦 ∈ { ∅ } 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑥 = ∅ )
10 velsn ⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
11 9 10 bitr4i ⊢ ( ∃ 𝑦 ∈ { ∅ } 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ 𝑥 ∈ { ∅ } )
12 3 11 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( { ∅ } ↾t 𝐴 ) ↔ 𝑥 ∈ { ∅ } ) )
13 12 eqrdv ⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } ↾t 𝐴 ) = { ∅ } )