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	$⊢ J ↾_{𝑡} A \in Top \to (J \in V \land A \in V)$

Step	Hyp	Ref	Expression
1		0opn	$⊢ J ↾_{𝑡} A \in Top \to \emptyset \in (J ↾_{𝑡} A)$
2		n0i	$⊢ \emptyset \in (J ↾_{𝑡} A) \to \neg J ↾_{𝑡} A = \emptyset$
3	1 2	syl	$⊢ J ↾_{𝑡} A \in Top \to \neg J ↾_{𝑡} A = \emptyset$
4		restfn	$⊢ ↾_{𝑡} Fn (V \times V)$
5	4	fndmi	$⊢ dom ↾_{𝑡} = V \times V$
6	5	ndmov	$⊢ \neg (J \in V \land A \in V) \to J ↾_{𝑡} A = \emptyset$
7	3 6	nsyl2	$⊢ J ↾_{𝑡} A \in Top \to (J \in V \land A \in V)$

Metamath Proof Explorer