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