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 ⊢ F = x ∈ ran ⁡ . ⟼ if x = ∅ 0 0 sup x ℝ * < sup x ℝ * <
Assertion ioorinv ⊢ A ∈ ran ⁡ . → . ⁡ F ⁡ A = A

Proof

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