Metamath Proof Explorer


Theorem ioorf

Description: Define a function from open intervals to their endpoints. (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 ioorf 𝐹 : 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 0le0 0 ≤ 0
7 df-br ( 0 ≤ 0 ↔ ⟨ 0 , 0 ⟩ ∈ ≤ )
8 6 7 mpbi ⟨ 0 , 0 ⟩ ∈ ≤
9 0xr 0 ∈ ℝ*
10 opelxpi ( ( 0 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ* × ℝ* ) )
11 9 9 10 mp2an ⟨ 0 , 0 ⟩ ∈ ( ℝ* × ℝ* )
12 8 11 elini ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ* × ℝ* ) )
13 12 a1i ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ 𝑥 = ∅ ) → ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
14 simplr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 = ( 𝑎 (,) 𝑏 ) )
15 14 infeq1d ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( 𝑥 , ℝ* , < ) = inf ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) )
16 simplll ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎 ∈ ℝ* )
17 simpllr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑏 ∈ ℝ* )
18 simpr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ¬ 𝑥 = ∅ )
19 18 neqned ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 ≠ ∅ )
20 14 19 eqnetrrd ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑎 (,) 𝑏 ) ≠ ∅ )
21 df-ioo (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )
22 idd ( ( 𝑤 ∈ ℝ*𝑏 ∈ ℝ* ) → ( 𝑤 < 𝑏𝑤 < 𝑏 ) )
23 xrltle ( ( 𝑤 ∈ ℝ*𝑏 ∈ ℝ* ) → ( 𝑤 < 𝑏𝑤𝑏 ) )
24 idd ( ( 𝑎 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝑎 < 𝑤𝑎 < 𝑤 ) )
25 xrltle ( ( 𝑎 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝑎 < 𝑤𝑎𝑤 ) )
26 21 22 23 24 25 ixxlb ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → inf ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) = 𝑎 )
27 16 17 20 26 syl3anc ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) = 𝑎 )
28 15 27 eqtrd ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( 𝑥 , ℝ* , < ) = 𝑎 )
29 14 supeq1d ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( 𝑥 , ℝ* , < ) = sup ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) )
30 21 22 23 24 25 ixxub ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → sup ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) = 𝑏 )
31 16 17 20 30 syl3anc ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( ( 𝑎 (,) 𝑏 ) , ℝ* , < ) = 𝑏 )
32 29 31 eqtrd ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( 𝑥 , ℝ* , < ) = 𝑏 )
33 28 32 opeq12d ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
34 ioon0 ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
35 34 ad2antrr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
36 20 35 mpbid ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎 < 𝑏 )
37 xrltle ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) → ( 𝑎 < 𝑏𝑎𝑏 ) )
38 37 ad2antrr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑎 < 𝑏𝑎𝑏 ) )
39 36 38 mpd ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎𝑏 )
40 df-br ( 𝑎𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ≤ )
41 39 40 sylib ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ≤ )
42 opelxpi ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ* × ℝ* ) )
43 42 ad2antrr ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ* × ℝ* ) )
44 41 43 elind ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
45 33 44 eqeltrd ( ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
46 13 45 ifclda ( ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
47 46 ex ( ( 𝑎 ∈ ℝ*𝑏 ∈ ℝ* ) → ( 𝑥 = ( 𝑎 (,) 𝑏 ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) ) )
48 47 rexlimivv ( ∃ 𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑥 = ( 𝑎 (,) 𝑏 ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
49 5 48 sylbi ( 𝑥 ∈ ran (,) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ* , < ) , sup ( 𝑥 , ℝ* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ* × ℝ* ) ) )
50 1 49 fmpti 𝐹 : ran (,) ⟶ ( ≤ ∩ ( ℝ* × ℝ* ) )