Theorem restrcl

Description: Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	restrcl	⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		0opn	⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ Top → ∅ ∈ ( 𝐽 ↾t 𝐴 ) )
2		n0i	⊢ ( ∅ ∈ ( 𝐽 ↾t 𝐴 ) → ¬ ( 𝐽 ↾t 𝐴 ) = ∅ )
3	1 2	syl	⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ Top → ¬ ( 𝐽 ↾t 𝐴 ) = ∅ )
4		restfn	⊢ ↾t Fn ( V × V )
5	4	fndmi	⊢ dom ↾t = ( V × V )
6	5	ndmov	⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ∅ )
7	3 6	nsyl2	⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )