Metamath Proof Explorer

Theorem ioorinv

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 ioorinv ( 𝐴 ∈ ran (,) → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ioorf.1 ⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
2 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
3 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
4 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝐴 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) ) )
5 2 3 4 mp2b ⊢ ( 𝐴 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) )
6 1 ioorinv2 ⊢ ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ )
7 6 fveq2d ⊢ ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → ( (,) ‘ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ) = ( (,) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
8 df-ov ⊢ ( 𝑎 (,) 𝑏 ) = ( (,) ‘ ⟨ 𝑎 , 𝑏 ⟩ )
9 7 8 eqtr4di ⊢ ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → ( (,) ‘ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ) = ( 𝑎 (,) 𝑏 ) )
10 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
11 neeq1 ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( 𝐴 ≠ ∅ ↔ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) )
12 10 11 bitr3id ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ¬ 𝐴 = ∅ ↔ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) )
13 2fveq3 ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ) )
14 id ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → 𝐴 = ( 𝑎 (,) 𝑏 ) )
15 13 14 eqeq12d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ↔ ( (,) ‘ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ) = ( 𝑎 (,) 𝑏 ) ) )
16 12 15 imbi12d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ¬ 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ) ↔ ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → ( (,) ‘ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ) = ( 𝑎 (,) 𝑏 ) ) ) )
17 9 16 mpbiri ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ¬ 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ) )
18 17 a1i ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ¬ 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ) ) )
19 18 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ¬ 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ) )
20 5 19 sylbi ⊢ ( 𝐴 ∈ ran (,) → ( ¬ 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 ) )
21 ioorebas ⊢ ( 0 (,) 0 ) ∈ ran (,)
22 1 ioorval ⊢ ( ( 0 (,) 0 ) ∈ ran (,) → ( 𝐹 ‘ ( 0 (,) 0 ) ) = if ( ( 0 (,) 0 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 0 (,) 0 ) , ℝ* , < ) , sup ( ( 0 (,) 0 ) , ℝ* , < ) ⟩ ) )
23 21 22 ax-mp ⊢ ( 𝐹 ‘ ( 0 (,) 0 ) ) = if ( ( 0 (,) 0 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 0 (,) 0 ) , ℝ* , < ) , sup ( ( 0 (,) 0 ) , ℝ* , < ) ⟩ )
24 iooid ⊢ ( 0 (,) 0 ) = ∅
25 24 iftruei ⊢ if ( ( 0 (,) 0 ) = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( ( 0 (,) 0 ) , ℝ* , < ) , sup ( ( 0 (,) 0 ) , ℝ* , < ) ⟩ ) = ⟨ 0 , 0 ⟩
26 23 25 eqtri ⊢ ( 𝐹 ‘ ( 0 (,) 0 ) ) = ⟨ 0 , 0 ⟩
27 26 fveq2i ⊢ ( (,) ‘ ( 𝐹 ‘ ( 0 (,) 0 ) ) ) = ( (,) ‘ ⟨ 0 , 0 ⟩ )
28 df-ov ⊢ ( 0 (,) 0 ) = ( (,) ‘ ⟨ 0 , 0 ⟩ )
29 27 28 eqtr4i ⊢ ( (,) ‘ ( 𝐹 ‘ ( 0 (,) 0 ) ) ) = ( 0 (,) 0 )
30 24 eqeq2i ⊢ ( 𝐴 = ( 0 (,) 0 ) ↔ 𝐴 = ∅ )
31 30 biimpri ⊢ ( 𝐴 = ∅ → 𝐴 = ( 0 (,) 0 ) )
32 31 fveq2d ⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 0 (,) 0 ) ) )
33 32 fveq2d ⊢ ( 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 0 (,) 0 ) ) ) )
34 29 33 31 3eqtr4a ⊢ ( 𝐴 = ∅ → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 )
35 20 34 pm2.61d2 ⊢ ( 𝐴 ∈ ran (,) → ( (,) ‘ ( 𝐹 ‘ 𝐴 ) ) = 𝐴 )