Metamath Proof Explorer


Theorem ioorinv2

Description: The function F is an "inverse" of sorts to the open interval function. (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 ioorinv2 ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐹 ‘ ( 𝐴 (,) 𝐵 ) ) = ⟨ 𝐴 , 𝐵 ⟩ )

Proof

Step Hyp Ref Expression
1 ioorf.1 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
2 ioorebas ( 𝐴 (,) 𝐵 ) ∈ ran (,)
3 1 ioorval ( ( 𝐴 (,) 𝐵 ) ∈ ran (,) → ( 𝐹 ‘ ( 𝐴 (,) 𝐵 ) ) = if ( ( 𝐴 (,) 𝐵 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ ) )
4 2 3 ax-mp ( 𝐹 ‘ ( 𝐴 (,) 𝐵 ) ) = if ( ( 𝐴 (,) 𝐵 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ )
5 ifnefalse ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → if ( ( 𝐴 (,) 𝐵 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ ) = ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ )
6 n0 ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
7 eliooxr ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) )
8 7 exlimiv ( ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) )
9 6 8 sylbi ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) )
10 9 simpld ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → 𝐴 ∈ ℝ* )
11 9 simprd ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → 𝐵 ∈ ℝ* )
12 id ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
13 df-ioo (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )
14 idd ( ( 𝑤 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵𝑤 < 𝐵 ) )
15 xrltle ( ( 𝑤 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵𝑤𝐵 ) )
16 idd ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤𝐴 < 𝑤 ) )
17 xrltle ( ( 𝐴 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤𝐴𝑤 ) )
18 13 14 15 16 17 ixxlb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
19 10 11 12 18 syl3anc ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
20 13 14 15 16 17 ixxub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
21 10 11 12 20 syl3anc ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
22 19 21 opeq12d ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
23 5 22 eqtrd ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → if ( ( 𝐴 (,) 𝐵 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) , sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
24 4 23 syl5eq ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐹 ‘ ( 𝐴 (,) 𝐵 ) ) = ⟨ 𝐴 , 𝐵 ⟩ )