Metamath Proof Explorer


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 ) )