Proof of Theorem gtinfOLD
Step | Hyp | Ref
| Expression |
1 | | simprl 794 |
. . 3
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → 𝐴 ∈ ℝ) |
2 | | gtso 10119 |
. . . . . . 7
⊢ ◡ < Or ℝ |
3 | 2 | supex 8369 |
. . . . . 6
⊢ sup(𝑆, ℝ, ◡ < ) ∈ V |
4 | | brcnvg 5303 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) ∈ V) → (𝐴◡
< sup(𝑆, ℝ, ◡ < ) ↔ sup(𝑆, ℝ, ◡ < ) < 𝐴)) |
5 | 3, 4 | mpan2 707 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴◡ < sup(𝑆, ℝ, ◡ < ) ↔ sup(𝑆, ℝ, ◡ < ) < 𝐴)) |
6 | 5 | biimpar 502 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴) → 𝐴◡
< sup(𝑆, ℝ, ◡ < )) |
7 | 6 | adantl 482 |
. . 3
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → 𝐴◡
< sup(𝑆, ℝ, ◡ < )) |
8 | 2 | a1i 11 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ◡ < Or ℝ) |
9 | | infm3 10982 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
10 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
11 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
12 | 10, 11 | brcnv 5305 |
. . . . . . . . . 10
⊢ (𝑥◡ < 𝑦 ↔ 𝑦 < 𝑥) |
13 | 12 | notbii 310 |
. . . . . . . . 9
⊢ (¬
𝑥◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥) |
14 | 13 | ralbii 2980 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑆 ¬ 𝑥◡
< 𝑦 ↔ ∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥) |
15 | 11, 10 | brcnv 5305 |
. . . . . . . . . 10
⊢ (𝑦◡ < 𝑥 ↔ 𝑥 < 𝑦) |
16 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
17 | 11, 16 | brcnv 5305 |
. . . . . . . . . . 11
⊢ (𝑦◡ < 𝑧 ↔ 𝑧 < 𝑦) |
18 | 17 | rexbii 3041 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑆 𝑦◡
< 𝑧 ↔ ∃𝑧 ∈ 𝑆 𝑧 < 𝑦) |
19 | 15, 18 | imbi12i 340 |
. . . . . . . . 9
⊢ ((𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦)) |
20 | 19 | ralbii 2980 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦)) |
21 | 14, 20 | anbi12i 733 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝑆 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧)) ↔
(∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
22 | 21 | rexbii 3041 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ (∀𝑦 ∈
𝑆 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧)) ↔
∃𝑥 ∈ ℝ
(∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
23 | 9, 22 | sylibr 224 |
. . . . 5
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧))) |
24 | 23 | adantr 481 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝑆 𝑦◡
< 𝑧))) |
25 | 8, 24 | suplub 8366 |
. . 3
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ((𝐴 ∈ ℝ ∧ 𝐴◡
< sup(𝑆, ℝ, ◡ < )) → ∃𝑧 ∈ 𝑆 𝐴◡
< 𝑧)) |
26 | 1, 7, 25 | mp2and 715 |
. 2
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝐴◡
< 𝑧) |
27 | | brcnvg 5303 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ V) → (𝐴◡ < 𝑧 ↔ 𝑧 < 𝐴)) |
28 | 16, 27 | mpan2 707 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴◡ < 𝑧 ↔ 𝑧 < 𝐴)) |
29 | 28 | rexbidv 3052 |
. . 3
⊢ (𝐴 ∈ ℝ →
(∃𝑧 ∈ 𝑆 𝐴◡
< 𝑧 ↔ ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)) |
30 | 29 | ad2antrl 764 |
. 2
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → (∃𝑧 ∈ 𝑆 𝐴◡
< 𝑧 ↔ ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)) |
31 | 26, 30 | mpbid 222 |
1
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝑧 < 𝐴) |