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 ⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐹 ‘ ( 𝐴 (,) 𝐵 ) ) = ⟨ 𝐴 , 𝐵 ⟩ )