Metamath Proof Explorer


Theorem elrest

Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion elrest ( ( 𝐽𝑉𝐵𝑊 ) → ( 𝐴 ∈ ( 𝐽t 𝐵 ) ↔ ∃ 𝑥𝐽 𝐴 = ( 𝑥𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 restval ( ( 𝐽𝑉𝐵𝑊 ) → ( 𝐽t 𝐵 ) = ran ( 𝑥𝐽 ↦ ( 𝑥𝐵 ) ) )
2 1 eleq2d ( ( 𝐽𝑉𝐵𝑊 ) → ( 𝐴 ∈ ( 𝐽t 𝐵 ) ↔ 𝐴 ∈ ran ( 𝑥𝐽 ↦ ( 𝑥𝐵 ) ) ) )
3 eqid ( 𝑥𝐽 ↦ ( 𝑥𝐵 ) ) = ( 𝑥𝐽 ↦ ( 𝑥𝐵 ) )
4 vex 𝑥 ∈ V
5 4 inex1 ( 𝑥𝐵 ) ∈ V
6 3 5 elrnmpti ( 𝐴 ∈ ran ( 𝑥𝐽 ↦ ( 𝑥𝐵 ) ) ↔ ∃ 𝑥𝐽 𝐴 = ( 𝑥𝐵 ) )
7 2 6 bitrdi ( ( 𝐽𝑉𝐵𝑊 ) → ( 𝐴 ∈ ( 𝐽t 𝐵 ) ↔ ∃ 𝑥𝐽 𝐴 = ( 𝑥𝐵 ) ) )