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