Metamath Proof Explorer

Theorem rest0

Description: The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion rest0 ⊢ J ∈ Top → J ↾ 𝑡 ∅ = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 restval ⊢ J ∈ Top ∧ ∅ ∈ V → J ↾ 𝑡 ∅ = ran ⁡ x ∈ J ⟼ x ∩ ∅
3 1 2 mpan2 ⊢ J ∈ Top → J ↾ 𝑡 ∅ = ran ⁡ x ∈ J ⟼ x ∩ ∅
4 in0 ⊢ x ∩ ∅ = ∅
5 1 elsn2 ⊢ x ∩ ∅ ∈ ∅ ↔ x ∩ ∅ = ∅
6 4 5 mpbir ⊢ x ∩ ∅ ∈ ∅
7 6 a1i ⊢ J ∈ Top ∧ x ∈ J → x ∩ ∅ ∈ ∅
8 7 fmpttd ⊢ J ∈ Top → x ∈ J ⟼ x ∩ ∅ : J ⟶ ∅
9 8 frnd ⊢ J ∈ Top → ran ⁡ x ∈ J ⟼ x ∩ ∅ ⊆ ∅
10 3 9 eqsstrd ⊢ J ∈ Top → J ↾ 𝑡 ∅ ⊆ ∅
11 resttop ⊢ J ∈ Top ∧ ∅ ∈ V → J ↾ 𝑡 ∅ ∈ Top
12 1 11 mpan2 ⊢ J ∈ Top → J ↾ 𝑡 ∅ ∈ Top
13 0opn ⊢ J ↾ 𝑡 ∅ ∈ Top → ∅ ∈ J ↾ 𝑡 ∅
14 12 13 syl ⊢ J ∈ Top → ∅ ∈ J ↾ 𝑡 ∅
15 14 snssd ⊢ J ∈ Top → ∅ ⊆ J ↾ 𝑡 ∅
16 10 15 eqssd ⊢ J ∈ Top → J ↾ 𝑡 ∅ = ∅