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 ( 𝐴 , ℝ* , < ) ⟩ ) )