Theorem elrestr

Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Assertion	elrestr	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽 ) → ( 𝐴 ∩ 𝑆 ) ∈ ( 𝐽 ↾t 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 ∩ 𝑆 ) = ( 𝐴 ∩ 𝑆 )
2		ineq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑆 ) = ( 𝐴 ∩ 𝑆 ) )
3	2	rspceeqv	⊢ ( ( 𝐴 ∈ 𝐽 ∧ ( 𝐴 ∩ 𝑆 ) = ( 𝐴 ∩ 𝑆 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∩ 𝑆 ) = ( 𝑥 ∩ 𝑆 ) )
4	1 3	mpan2	⊢ ( 𝐴 ∈ 𝐽 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∩ 𝑆 ) = ( 𝑥 ∩ 𝑆 ) )
5		elrest	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝐴 ∩ 𝑆 ) ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∩ 𝑆 ) = ( 𝑥 ∩ 𝑆 ) ) )
6	4 5	imbitrrid	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐴 ∈ 𝐽 → ( 𝐴 ∩ 𝑆 ) ∈ ( 𝐽 ↾t 𝑆 ) ) )
7	6	3impia	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽 ) → ( 𝐴 ∩ 𝑆 ) ∈ ( 𝐽 ↾t 𝑆 ) )