Step | Hyp | Ref
| Expression |
1 | | ioorf.1 |
. 2
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉)) |
2 | | ioof 12271 |
. . . 4
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
3 | | ffn 6045 |
. . . 4
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
4 | | ovelrn 6810 |
. . . 4
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑥 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑥 =
(𝑎(,)𝑏))) |
5 | 2, 3, 4 | mp2b 10 |
. . 3
⊢ (𝑥 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎(,)𝑏)) |
6 | | 0le0 11110 |
. . . . . . . . 9
⊢ 0 ≤
0 |
7 | | df-br 4654 |
. . . . . . . . 9
⊢ (0 ≤ 0
↔ 〈0, 0〉 ∈ ≤ ) |
8 | 6, 7 | mpbi 220 |
. . . . . . . 8
⊢ 〈0,
0〉 ∈ ≤ |
9 | | 0xr 10086 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
10 | | opelxpi 5148 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 0 ∈ ℝ*) → 〈0,
0〉 ∈ (ℝ* ×
ℝ*)) |
11 | 9, 9, 10 | mp2an 708 |
. . . . . . . 8
⊢ 〈0,
0〉 ∈ (ℝ* ×
ℝ*) |
12 | | elin 3796 |
. . . . . . . 8
⊢ (〈0,
0〉 ∈ ( ≤ ∩ (ℝ* × ℝ*))
↔ (〈0, 0〉 ∈ ≤ ∧ 〈0, 0〉 ∈
(ℝ* × ℝ*))) |
13 | 8, 11, 12 | mpbir2an 955 |
. . . . . . 7
⊢ 〈0,
0〉 ∈ ( ≤ ∩ (ℝ* ×
ℝ*)) |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ 𝑥 = ∅) → 〈0, 0〉 ∈ (
≤ ∩ (ℝ* × ℝ*))) |
15 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑥 = (𝑎(,)𝑏)) |
16 | 15 | infeq1d 8383 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf(𝑥, ℝ*, < ) = inf((𝑎(,)𝑏), ℝ*, <
)) |
17 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 ∈ ℝ*) |
18 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑏 ∈ ℝ*) |
19 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → ¬ 𝑥 = ∅) |
20 | 19 | neqned 2801 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅) |
21 | 15, 20 | eqnetrrd 2862 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → (𝑎(,)𝑏) ≠ ∅) |
22 | | df-ioo 12179 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
23 | | idd 24 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑤 < 𝑏 → 𝑤 < 𝑏)) |
24 | | xrltle 11982 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑤 < 𝑏 → 𝑤 ≤ 𝑏)) |
25 | | idd 24 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑎 < 𝑤 → 𝑎 < 𝑤)) |
26 | | xrltle 11982 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑎 < 𝑤 → 𝑎 ≤ 𝑤)) |
27 | 22, 23, 24, 25, 26 | ixxlb 12197 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ (𝑎(,)𝑏) ≠ ∅) → inf((𝑎(,)𝑏), ℝ*, < ) = 𝑎) |
28 | 17, 18, 21, 27 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf((𝑎(,)𝑏), ℝ*, < ) = 𝑎) |
29 | 16, 28 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf(𝑥, ℝ*, < ) = 𝑎) |
30 | 15 | supeq1d 8352 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup(𝑥, ℝ*, < ) = sup((𝑎(,)𝑏), ℝ*, <
)) |
31 | 22, 23, 24, 25, 26 | ixxub 12196 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ (𝑎(,)𝑏) ≠ ∅) → sup((𝑎(,)𝑏), ℝ*, < ) = 𝑏) |
32 | 17, 18, 21, 31 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup((𝑎(,)𝑏), ℝ*, < ) = 𝑏) |
33 | 30, 32 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup(𝑥, ℝ*, < ) = 𝑏) |
34 | 29, 33 | opeq12d 4410 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉 = 〈𝑎,
𝑏〉) |
35 | | ioon0 12201 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
36 | 35 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
37 | 21, 36 | mpbid 222 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 < 𝑏) |
38 | | xrltle 11982 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎 < 𝑏 → 𝑎 ≤ 𝑏)) |
39 | 38 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → (𝑎 < 𝑏 → 𝑎 ≤ 𝑏)) |
40 | 37, 39 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 ≤ 𝑏) |
41 | | df-br 4654 |
. . . . . . . . 9
⊢ (𝑎 ≤ 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ≤ ) |
42 | 40, 41 | sylib 208 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ ≤ ) |
43 | | opelxpi 5148 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → 〈𝑎, 𝑏〉 ∈ (ℝ* ×
ℝ*)) |
44 | 43 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ (ℝ* ×
ℝ*)) |
45 | 42, 44 | elind 3798 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ ( ≤ ∩
(ℝ* × ℝ*))) |
46 | 34, 45 | eqeltrd 2701 |
. . . . . 6
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉 ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
47 | 14, 46 | ifclda 4120 |
. . . . 5
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
48 | 47 | ex 450 |
. . . 4
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 = (𝑎(,)𝑏) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*)))) |
49 | 48 | rexlimivv 3036 |
. . 3
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎(,)𝑏) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
50 | 5, 49 | sylbi 207 |
. 2
⊢ (𝑥 ∈ ran (,) → if(𝑥 = ∅, 〈0, 0〉,
〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, < )〉) ∈ (
≤ ∩ (ℝ* × ℝ*))) |
51 | 1, 50 | fmpti 6383 |
1
⊢ 𝐹:ran (,)⟶( ≤ ∩
(ℝ* × ℝ*)) |