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

Metamath Proof Explorer

Theorem ioorval

Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypothesis ioorf.1 ⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
Assertion ioorval ( 𝐴 ∈ ran (,) → ( 𝐹 ‘ 𝐴 ) = if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 ioorf.1 ⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
2 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∅ ↔ 𝐴 = ∅ ) )
3 infeq1 ⊢ ( 𝑥 = 𝐴 → inf ( 𝑥 , ℝ* , < ) = inf ( 𝐴 , ℝ* , < ) )
4 supeq1 ⊢ ( 𝑥 = 𝐴 → sup ( 𝑥 , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )
5 3 4 opeq12d ⊢ ( 𝑥 = 𝐴 → ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ = ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ )
6 2 5 ifbieq2d ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) = if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) )
7 opex ⊢ ⟨ 0 , 0 ⟩ ∈ V
8 opex ⊢ ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ∈ V
9 7 8 ifex ⊢ if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) ∈ V
10 6 1 9 fvmpt ⊢ ( 𝐴 ∈ ran (,) → ( 𝐹 ‘ 𝐴 ) = if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) )