Proof of Theorem uzsupss
Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ ℤ) |
2 | | uzid 12597 |
. . . . 5
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ (ℤ≥‘𝑀)) |
4 | | uzsupss.1 |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | 3, 4 | eleqtrrdi 2850 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ 𝑍) |
6 | | ral0 4443 |
. . . 4
⊢
∀𝑦 ∈
∅ ¬ 𝑀 < 𝑦 |
7 | | simpr 485 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝐴 = ∅) |
8 | 7 | raleqdv 3348 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ↔ ∀𝑦 ∈ ∅ ¬ 𝑀 < 𝑦)) |
9 | 6, 8 | mpbiri 257 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦) |
10 | | eluzle 12595 |
. . . . . . . 8
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑦) |
11 | | eluzel2 12587 |
. . . . . . . . 9
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
12 | | eluzelz 12592 |
. . . . . . . . 9
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑦 ∈ ℤ) |
13 | | zre 12323 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
14 | | zre 12323 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
15 | | lenlt 11053 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) |
16 | 13, 14, 15 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) |
17 | 11, 12, 16 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) |
18 | 10, 17 | mpbid 231 |
. . . . . . 7
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → ¬ 𝑦 < 𝑀) |
19 | 18, 4 | eleq2s 2857 |
. . . . . 6
⊢ (𝑦 ∈ 𝑍 → ¬ 𝑦 < 𝑀) |
20 | 19 | pm2.21d 121 |
. . . . 5
⊢ (𝑦 ∈ 𝑍 → (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) |
21 | 20 | rgen 3074 |
. . . 4
⊢
∀𝑦 ∈
𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) |
22 | 21 | a1i 11 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) |
23 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝑥 < 𝑦 ↔ 𝑀 < 𝑦)) |
24 | 23 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑀 < 𝑦)) |
25 | 24 | ralbidv 3112 |
. . . . 5
⊢ (𝑥 = 𝑀 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦)) |
26 | | breq2 5078 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑀)) |
27 | 26 | imbi1d 342 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
28 | 27 | ralbidv 3112 |
. . . . 5
⊢ (𝑥 = 𝑀 → (∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
29 | 25, 28 | anbi12d 631 |
. . . 4
⊢ (𝑥 = 𝑀 → ((∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))) |
30 | 29 | rspcev 3561 |
. . 3
⊢ ((𝑀 ∈ 𝑍 ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
31 | 5, 9, 22, 30 | syl12anc 834 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
32 | | simpl2 1191 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ 𝑍) |
33 | | uzssz 12603 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
34 | 4, 33 | eqsstri 3955 |
. . . . 5
⊢ 𝑍 ⊆
ℤ |
35 | 32, 34 | sstrdi 3933 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ ℤ) |
36 | | simpr 485 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
37 | | simpl3 1192 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
38 | | zsupss 12677 |
. . . 4
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
39 | 35, 36, 37, 38 | syl3anc 1370 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
40 | | ssrexv 3988 |
. . 3
⊢ (𝐴 ⊆ 𝑍 → (∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))) |
41 | 32, 39, 40 | sylc 65 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
42 | 31, 41 | pm2.61dane 3032 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |