Theorem elrestd

Description: A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	elrestd.1	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
	elrestd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	elrestd.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
	elrestd.4	⊢ 𝐴 = ( 𝑋 ∩ 𝐵 )
Assertion	elrestd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elrestd.1	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
2		elrestd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		elrestd.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
4		elrestd.4	⊢ 𝐴 = ( 𝑋 ∩ 𝐵 )
5	4	a1i	⊢ ( 𝜑 → 𝐴 = ( 𝑋 ∩ 𝐵 ) )
6		ineq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∩ 𝐵 ) = ( 𝑋 ∩ 𝐵 ) )
7	6	rspceeqv	⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐴 = ( 𝑋 ∩ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐵 ) )
8	3 5 7	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐵 ) )
9		elrest	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐵 ) ) )
10	1 2 9	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐵 ) ) )
11	8 10	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐵 ) )