This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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