Metamath Proof Explorer

Theorem ioorcl

Description: The function F does not always return real numbers, but it does on intervals of finite volume. (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 ioorcl ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )

Proof

Step Hyp Ref Expression
1 ioorf.1 ⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) )
2 1 ioorf ⊢ 𝐹 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) )
3 2 ffvelrni ⊢ ( 𝐴 ∈ ran (,) → ( 𝐹 ‘ 𝐴 ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
4 3 adantr ⊢ ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
5 4 elin1d ⊢ ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ≤ )
6 1 ioorval ⊢ ( 𝐴 ∈ ran (,) → ( 𝐹 ‘ 𝐴 ) = if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) = if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) )
8 iftrue ⊢ ( 𝐴 = ∅ → if ( 𝐴 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝐴 , ℝ* , < ) , sup ( 𝐴 , ℝ* , < ) ⟩ ) = ⟨ 0 , 0 ⟩ )
9 7 8 sylan9eq ⊢ ( ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ 𝐴 = ∅ ) → ( 𝐹 ‘ 𝐴 ) = ⟨ 0 , 0 ⟩ )
10 0re ⊢ 0 ∈ ℝ
11 opelxpi ⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ ) )
12 10 10 11 mp2an ⊢ ⟨ 0 , 0 ⟩ ∈ ( ℝ × ℝ )
13 9 12 eqeltrdi ⊢ ( ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ 𝐴 = ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) )
14 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
15 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
16 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝐴 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) ) )
17 14 15 16 mp2b ⊢ ( 𝐴 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) )
18 1 ioorinv2 ⊢ ( ( 𝑎 (,) 𝑏 ) ≠ ∅ → ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ )
19 18 adantl ⊢ ( ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ )
20 ioorcl2 ⊢ ( ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ∧ ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
21 20 ancoms ⊢ ( ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
22 opelxpi ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ × ℝ ) )
23 21 22 syl ⊢ ( ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ × ℝ ) )
24 19 23 eqeltrd ⊢ ( ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ( ℝ × ℝ ) )
25 fveq2 ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( vol* ‘ 𝐴 ) = ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) )
26 25 eleq1d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ) )
27 neeq1 ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( 𝐴 ≠ ∅ ↔ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) )
28 26 27 anbi12d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) ↔ ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) ) )
29 fveq2 ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) )
30 29 eleq1d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ↔ ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ( ℝ × ℝ ) ) )
31 28 30 imbi12d ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ) ↔ ( ( ( vol* ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ℝ ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → ( 𝐹 ‘ ( 𝑎 (,) 𝑏 ) ) ∈ ( ℝ × ℝ ) ) ) )
32 24 31 mpbiri ⊢ ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ) )
33 32 a1i ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ) ) )
34 33 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝐴 = ( 𝑎 (,) 𝑏 ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ) )
35 17 34 sylbi ⊢ ( 𝐴 ∈ ran (,) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) ) )
36 35 impl ⊢ ( ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) )
37 13 36 pm2.61dane ⊢ ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ℝ × ℝ ) )
38 5 37 elind ⊢ ( ( 𝐴 ∈ ran (,) ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )