Proof of Theorem uzsupss
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1191 | . . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ ℤ) | 
| 2 |  | uzid 12894 | . . . . 5
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ (ℤ≥‘𝑀)) | 
| 4 |  | uzsupss.1 | . . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 5 | 3, 4 | eleqtrrdi 2851 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝑀 ∈ 𝑍) | 
| 6 |  | ral0 4512 | . . . 4
⊢
∀𝑦 ∈
∅ ¬ 𝑀 < 𝑦 | 
| 7 |  | simpr 484 | . . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → 𝐴 = ∅) | 
| 8 | 7 | raleqdv 3325 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ↔ ∀𝑦 ∈ ∅ ¬ 𝑀 < 𝑦)) | 
| 9 | 6, 8 | mpbiri 258 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦) | 
| 10 |  | eluzle 12892 | . . . . . . . 8
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑦) | 
| 11 |  | eluzel2 12884 | . . . . . . . . 9
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 12 |  | eluzelz 12889 | . . . . . . . . 9
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → 𝑦 ∈ ℤ) | 
| 13 |  | zre 12619 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 14 |  | zre 12619 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) | 
| 15 |  | lenlt 11340 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) | 
| 16 | 13, 14, 15 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) | 
| 17 | 11, 12, 16 | syl2anc 584 | . . . . . . . 8
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → (𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀)) | 
| 18 | 10, 17 | mpbid 232 | . . . . . . 7
⊢ (𝑦 ∈
(ℤ≥‘𝑀) → ¬ 𝑦 < 𝑀) | 
| 19 | 18, 4 | eleq2s 2858 | . . . . . 6
⊢ (𝑦 ∈ 𝑍 → ¬ 𝑦 < 𝑀) | 
| 20 | 19 | pm2.21d 121 | . . . . 5
⊢ (𝑦 ∈ 𝑍 → (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) | 
| 21 | 20 | rgen 3062 | . . . 4
⊢
∀𝑦 ∈
𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) | 
| 22 | 21 | a1i 11 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) | 
| 23 |  | breq1 5145 | . . . . . . 7
⊢ (𝑥 = 𝑀 → (𝑥 < 𝑦 ↔ 𝑀 < 𝑦)) | 
| 24 | 23 | notbid 318 | . . . . . 6
⊢ (𝑥 = 𝑀 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑀 < 𝑦)) | 
| 25 | 24 | ralbidv 3177 | . . . . 5
⊢ (𝑥 = 𝑀 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦)) | 
| 26 |  | breq2 5146 | . . . . . . 7
⊢ (𝑥 = 𝑀 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑀)) | 
| 27 | 26 | imbi1d 341 | . . . . . 6
⊢ (𝑥 = 𝑀 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 28 | 27 | ralbidv 3177 | . . . . 5
⊢ (𝑥 = 𝑀 → (∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 29 | 25, 28 | anbi12d 632 | . . . 4
⊢ (𝑥 = 𝑀 → ((∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))) | 
| 30 | 29 | rspcev 3621 | . . 3
⊢ ((𝑀 ∈ 𝑍 ∧ (∀𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑀 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 31 | 5, 9, 22, 30 | syl12anc 836 | . 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 = ∅) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 32 |  | simpl2 1192 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ 𝑍) | 
| 33 |  | uzssz 12900 | . . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ | 
| 34 | 4, 33 | eqsstri 4029 | . . . . 5
⊢ 𝑍 ⊆
ℤ | 
| 35 | 32, 34 | sstrdi 3995 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ ℤ) | 
| 36 |  | simpr 484 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) | 
| 37 |  | simpl3 1193 | . . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) | 
| 38 |  | zsupss 12980 | . . . 4
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 39 | 35, 36, 37, 38 | syl3anc 1372 | . . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 40 |  | ssrexv 4052 | . . 3
⊢ (𝐴 ⊆ 𝑍 → (∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))) | 
| 41 | 32, 39, 40 | sylc 65 | . 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | 
| 42 | 31, 41 | pm2.61dane 3028 | 1
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |