| Step | Hyp | Ref
| Expression |
| 1 | | ioorf.1 |
. 2
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉)) |
| 2 | | ioof 13487 |
. . . 4
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 3 | | ffn 6736 |
. . . 4
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 4 | | ovelrn 7609 |
. . . 4
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑥 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑥 =
(𝑎(,)𝑏))) |
| 5 | 2, 3, 4 | mp2b 10 |
. . 3
⊢ (𝑥 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎(,)𝑏)) |
| 6 | | 0le0 12367 |
. . . . . . . . 9
⊢ 0 ≤
0 |
| 7 | | df-br 5144 |
. . . . . . . . 9
⊢ (0 ≤ 0
↔ 〈0, 0〉 ∈ ≤ ) |
| 8 | 6, 7 | mpbi 230 |
. . . . . . . 8
⊢ 〈0,
0〉 ∈ ≤ |
| 9 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 10 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 0 ∈ ℝ*) → 〈0,
0〉 ∈ (ℝ* ×
ℝ*)) |
| 11 | 9, 9, 10 | mp2an 692 |
. . . . . . . 8
⊢ 〈0,
0〉 ∈ (ℝ* ×
ℝ*) |
| 12 | 8, 11 | elini 4199 |
. . . . . . 7
⊢ 〈0,
0〉 ∈ ( ≤ ∩ (ℝ* ×
ℝ*)) |
| 13 | 12 | a1i 11 |
. . . . . 6
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ 𝑥 = ∅) → 〈0, 0〉 ∈ (
≤ ∩ (ℝ* × ℝ*))) |
| 14 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑥 = (𝑎(,)𝑏)) |
| 15 | 14 | infeq1d 9517 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf(𝑥, ℝ*, < ) = inf((𝑎(,)𝑏), ℝ*, <
)) |
| 16 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 ∈ ℝ*) |
| 17 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑏 ∈ ℝ*) |
| 18 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → ¬ 𝑥 = ∅) |
| 19 | 18 | neqned 2947 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅) |
| 20 | 14, 19 | eqnetrrd 3009 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → (𝑎(,)𝑏) ≠ ∅) |
| 21 | | df-ioo 13391 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 22 | | idd 24 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑤 < 𝑏 → 𝑤 < 𝑏)) |
| 23 | | xrltle 13191 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑤 < 𝑏 → 𝑤 ≤ 𝑏)) |
| 24 | | idd 24 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑎 < 𝑤 → 𝑎 < 𝑤)) |
| 25 | | xrltle 13191 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑎 < 𝑤 → 𝑎 ≤ 𝑤)) |
| 26 | 21, 22, 23, 24, 25 | ixxlb 13409 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ (𝑎(,)𝑏) ≠ ∅) → inf((𝑎(,)𝑏), ℝ*, < ) = 𝑎) |
| 27 | 16, 17, 20, 26 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf((𝑎(,)𝑏), ℝ*, < ) = 𝑎) |
| 28 | 15, 27 | eqtrd 2777 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → inf(𝑥, ℝ*, < ) = 𝑎) |
| 29 | 14 | supeq1d 9486 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup(𝑥, ℝ*, < ) = sup((𝑎(,)𝑏), ℝ*, <
)) |
| 30 | 21, 22, 23, 24, 25 | ixxub 13408 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ (𝑎(,)𝑏) ≠ ∅) → sup((𝑎(,)𝑏), ℝ*, < ) = 𝑏) |
| 31 | 16, 17, 20, 30 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup((𝑎(,)𝑏), ℝ*, < ) = 𝑏) |
| 32 | 29, 31 | eqtrd 2777 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → sup(𝑥, ℝ*, < ) = 𝑏) |
| 33 | 28, 32 | opeq12d 4881 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉 = 〈𝑎,
𝑏〉) |
| 34 | | ioon0 13413 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
| 36 | 20, 35 | mpbid 232 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 < 𝑏) |
| 37 | | xrltle 13191 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑎 < 𝑏 → 𝑎 ≤ 𝑏)) |
| 38 | 37 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → (𝑎 < 𝑏 → 𝑎 ≤ 𝑏)) |
| 39 | 36, 38 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 𝑎 ≤ 𝑏) |
| 40 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑎 ≤ 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ≤ ) |
| 41 | 39, 40 | sylib 218 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ ≤ ) |
| 42 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → 〈𝑎, 𝑏〉 ∈ (ℝ* ×
ℝ*)) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ (ℝ* ×
ℝ*)) |
| 44 | 41, 43 | elind 4200 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈𝑎, 𝑏〉 ∈ ( ≤ ∩
(ℝ* × ℝ*))) |
| 45 | 33, 44 | eqeltrd 2841 |
. . . . . 6
⊢ ((((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) ∧ ¬ 𝑥 = ∅) → 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉 ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
| 46 | 13, 45 | ifclda 4561 |
. . . . 5
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝑥 = (𝑎(,)𝑏)) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
| 47 | 46 | ex 412 |
. . . 4
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝑥 = (𝑎(,)𝑏) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*)))) |
| 48 | 47 | rexlimivv 3201 |
. . 3
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎(,)𝑏) → if(𝑥 = ∅, 〈0, 0〉, 〈inf(𝑥, ℝ*, < ),
sup(𝑥, ℝ*,
< )〉) ∈ ( ≤ ∩ (ℝ* ×
ℝ*))) |
| 49 | 5, 48 | sylbi 217 |
. 2
⊢ (𝑥 ∈ ran (,) → if(𝑥 = ∅, 〈0, 0〉,
〈inf(𝑥,
ℝ*, < ), sup(𝑥, ℝ*, < )〉) ∈ (
≤ ∩ (ℝ* × ℝ*))) |
| 50 | 1, 49 | fmpti 7132 |
1
⊢ 𝐹:ran (,)⟶( ≤ ∩
(ℝ* × ℝ*)) |