Metamath Proof Explorer


Theorem opncldf2

Description: The values of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009) (Proof shortened by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses opncldf.1 𝑋 = 𝐽
opncldf.2 𝐹 = ( 𝑢𝐽 ↦ ( 𝑋𝑢 ) )
Assertion opncldf2 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → ( 𝐹𝐴 ) = ( 𝑋𝐴 ) )

Proof

Step Hyp Ref Expression
1 opncldf.1 𝑋 = 𝐽
2 opncldf.2 𝐹 = ( 𝑢𝐽 ↦ ( 𝑋𝑢 ) )
3 difeq2 ( 𝑢 = 𝐴 → ( 𝑋𝑢 ) = ( 𝑋𝐴 ) )
4 simpr ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → 𝐴𝐽 )
5 1 opncld ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → ( 𝑋𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
6 2 3 4 5 fvmptd3 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → ( 𝐹𝐴 ) = ( 𝑋𝐴 ) )