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	$$⊢F=\left(x\in \mathrm{ran}\left(.\right)⟼if\left(x=\varnothing ,⟨0,0⟩,⟨sup\left(x,{ℝ}^{*},<\right),sup\left(x,{ℝ}^{*},<\right)⟩\right)\right)$$
Assertion	ioorval	$$⊢A\in \mathrm{ran}\left(.\right)\to F\left(A\right)=if\left(A=\varnothing ,⟨0,0⟩,⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	$$⊢F=\left(x\in \mathrm{ran}\left(.\right)⟼if\left(x=\varnothing ,⟨0,0⟩,⟨sup\left(x,{ℝ}^{*},<\right),sup\left(x,{ℝ}^{*},<\right)⟩\right)\right)$$
2		eqeq1	$$⊢x=A\to \left(x=\varnothing \leftrightarrow A=\varnothing \right)$$
3		infeq1	$$⊢x=A\to sup\left(x,{ℝ}^{*},<\right)=sup\left(A,{ℝ}^{*},<\right)$$
4		supeq1	$$⊢x=A\to sup\left(x,{ℝ}^{*},<\right)=sup\left(A,{ℝ}^{*},<\right)$$
5	3 4	opeq12d	$$⊢x=A\to ⟨sup\left(x,{ℝ}^{*},<\right),sup\left(x,{ℝ}^{*},<\right)⟩=⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩$$
6	2 5	ifbieq2d	$$⊢x=A\to if\left(x=\varnothing ,⟨0,0⟩,⟨sup\left(x,{ℝ}^{*},<\right),sup\left(x,{ℝ}^{*},<\right)⟩\right)=if\left(A=\varnothing ,⟨0,0⟩,⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩\right)$$
7		opex	$$⊢⟨0,0⟩\in \mathrm{V}$$
8		opex	$$⊢⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩\in \mathrm{V}$$
9	7 8	ifex	$$⊢if\left(A=\varnothing ,⟨0,0⟩,⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩\right)\in \mathrm{V}$$
10	6 1 9	fvmpt	$$⊢A\in \mathrm{ran}\left(.\right)\to F\left(A\right)=if\left(A=\varnothing ,⟨0,0⟩,⟨sup\left(A,{ℝ}^{*},<\right),sup\left(A,{ℝ}^{*},<\right)⟩\right)$$