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 𝐴 ) = { ∅ } )