Proof of Theorem sn-sup2
Step | Hyp | Ref
| Expression |
1 | | peano2re 10836 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
2 | 1 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → (𝑥 + 1) ∈ ℝ) |
3 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ → ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → (𝑥 + 1) ∈ ℝ)) |
4 | | ssel 3881 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ ℝ → (𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ)) |
5 | | sn-ltp1 39915 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
6 | 1 | ancli 553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈
ℝ)) |
7 | | lttr 10740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
((𝑦 < 𝑥 ∧ 𝑥 < (𝑥 + 1)) → 𝑦 < (𝑥 + 1))) |
8 | 7 | 3expb 1118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ)) →
((𝑦 < 𝑥 ∧ 𝑥 < (𝑥 + 1)) → 𝑦 < (𝑥 + 1))) |
9 | 6, 8 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦 < 𝑥 ∧ 𝑥 < (𝑥 + 1)) → 𝑦 < (𝑥 + 1))) |
10 | 5, 9 | sylan2i 609 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦 < 𝑥 ∧ 𝑥 ∈ ℝ) → 𝑦 < (𝑥 + 1))) |
11 | 10 | exp4b 435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → (𝑦 < 𝑥 → (𝑥 ∈ ℝ → 𝑦 < (𝑥 + 1))))) |
12 | 11 | com34 91 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → (𝑥 ∈ ℝ → (𝑦 < 𝑥 → 𝑦 < (𝑥 + 1))))) |
13 | 12 | pm2.43d 53 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → (𝑦 < 𝑥 → 𝑦 < (𝑥 + 1)))) |
14 | 13 | imp 411 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 → 𝑦 < (𝑥 + 1))) |
15 | | breq1 5028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (𝑦 < (𝑥 + 1) ↔ 𝑥 < (𝑥 + 1))) |
16 | 5, 15 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → (𝑦 = 𝑥 → 𝑦 < (𝑥 + 1))) |
17 | 16 | adantl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 = 𝑥 → 𝑦 < (𝑥 + 1))) |
18 | 14, 17 | jaod 857 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → 𝑦 < (𝑥 + 1))) |
19 | 18 | ex 417 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → ((𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → 𝑦 < (𝑥 + 1)))) |
20 | 4, 19 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ ℝ → (𝑦 ∈ 𝐴 → (𝑥 ∈ ℝ → ((𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → 𝑦 < (𝑥 + 1))))) |
21 | 20 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ ℝ → (𝑥 ∈ ℝ → (𝑦 ∈ 𝐴 → ((𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → 𝑦 < (𝑥 + 1))))) |
22 | 21 | imp 411 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 ∈ 𝐴 → ((𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → 𝑦 < (𝑥 + 1)))) |
23 | 22 | a2d 29 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦 ∈ 𝐴 → (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → (𝑦 ∈ 𝐴 → 𝑦 < (𝑥 + 1)))) |
24 | 23 | ralimdv2 3105 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1))) |
25 | 24 | expimpd 458 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ → ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1))) |
26 | 3, 25 | jcad 517 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ → ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ((𝑥 + 1) ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1)))) |
27 | | ovex 7176 |
. . . . . . . . . 10
⊢ (𝑥 + 1) ∈ V |
28 | | eleq1 2838 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 + 1) → (𝑧 ∈ ℝ ↔ (𝑥 + 1) ∈ ℝ)) |
29 | | breq2 5029 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 + 1) → (𝑦 < 𝑧 ↔ 𝑦 < (𝑥 + 1))) |
30 | 29 | ralbidv 3124 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 + 1) → (∀𝑦 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1))) |
31 | 28, 30 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 + 1) → ((𝑧 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑧) ↔ ((𝑥 + 1) ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1)))) |
32 | 27, 31 | spcev 3523 |
. . . . . . . . 9
⊢ (((𝑥 + 1) ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 < (𝑥 + 1)) → ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑧)) |
33 | 26, 32 | syl6 35 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ → ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑧))) |
34 | 33 | exlimdv 1935 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∃𝑥(𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑧(𝑧 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑧))) |
35 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧 ∈ ℝ ↔ 𝑥 ∈ ℝ)) |
36 | | breq2 5029 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑥)) |
37 | 36 | ralbidv 3124 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
38 | 35, 37 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ((𝑧 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑧) ↔ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥))) |
39 | 38 | cbvexvw 2045 |
. . . . . . 7
⊢
(∃𝑧(𝑧 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 < 𝑧) ↔ ∃𝑥(𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
40 | 34, 39 | syl6ib 254 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∃𝑥(𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥(𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥))) |
41 | | df-rex 3074 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) ↔ ∃𝑥(𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥))) |
42 | | df-rex 3074 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
𝐴 𝑦 < 𝑥 ↔ ∃𝑥(𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
43 | 40, 41, 42 | 3imtr4g 300 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
44 | 43 | adantr 485 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
45 | 44 | imdistani 573 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
46 | | df-3an 1087 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) ↔ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥))) |
47 | | df-3an 1087 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
48 | 45, 46, 47 | 3imtr4i 296 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
49 | | axsup 10739 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
50 | 48, 49 | syl 17 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |