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

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 ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) = { ∅ } )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 restval ⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ V ) → ( 𝐽 ↾t ∅ ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ ∅ ) ) )
3 1 2 mpan2 ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ ∅ ) ) )
4 in0 ⊢ ( 𝑥 ∩ ∅ ) = ∅
5 1 elsn2 ⊢ ( ( 𝑥 ∩ ∅ ) ∈ { ∅ } ↔ ( 𝑥 ∩ ∅ ) = ∅ )
6 4 5 mpbir ⊢ ( 𝑥 ∩ ∅ ) ∈ { ∅ }
7 6 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ ∅ ) ∈ { ∅ } )
8 7 fmpttd ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ ∅ ) ) : 𝐽 ⟶ { ∅ } )
9 8 frnd ⊢ ( 𝐽 ∈ Top → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ ∅ ) ) ⊆ { ∅ } )
10 3 9 eqsstrd ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) ⊆ { ∅ } )
11 resttop ⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ V ) → ( 𝐽 ↾t ∅ ) ∈ Top )
12 1 11 mpan2 ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) ∈ Top )
13 0opn ⊢ ( ( 𝐽 ↾t ∅ ) ∈ Top → ∅ ∈ ( 𝐽 ↾t ∅ ) )
14 12 13 syl ⊢ ( 𝐽 ∈ Top → ∅ ∈ ( 𝐽 ↾t ∅ ) )
15 14 snssd ⊢ ( 𝐽 ∈ Top → { ∅ } ⊆ ( 𝐽 ↾t ∅ ) )
16 10 15 eqssd ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) = { ∅ } )