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