Metamath Proof Explorer

Theorem uzsupss

Description: Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis uzsupss.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion uzsupss ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 uzsupss.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 simpl1 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → 𝑀 ∈ ℤ )
3 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 2 3 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 4 1 eleqtrrdi ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → 𝑀 ∈ 𝑍 )
6 ral0 ⊢ ∀ 𝑦 ∈ ∅ ¬ 𝑀 < 𝑦
7 simpr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
8 7 raleqdv ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ↔ ∀ 𝑦 ∈ ∅ ¬ 𝑀 < 𝑦 ) )
9 6 8 mpbiri ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 )
10 eluzle ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑦 )
11 eluzel2 ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑦 ∈ ℤ )
13 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
14 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
15 lenlt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀 ) )
16 13 14 15 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀 ) )
17 11 12 16 syl2anc ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑀 ) )
18 10 17 mpbid ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑀 ) → ¬ 𝑦 < 𝑀 )
19 18 1 eleq2s ⊢ ( 𝑦 ∈ 𝑍 → ¬ 𝑦 < 𝑀 )
20 19 pm2.21d ⊢ ( 𝑦 ∈ 𝑍 → ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
21 20 rgen ⊢ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
22 21 a1i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
23 breq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 < 𝑦 ↔ 𝑀 < 𝑦 ) )
24 23 notbid ⊢ ( 𝑥 = 𝑀 → ( ¬ 𝑥 < 𝑦 ↔ ¬ 𝑀 < 𝑦 ) )
25 24 ralbidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ) )
26 breq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑀 ) )
27 26 imbi1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
28 27 ralbidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
29 25 28 anbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
30 29 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑀 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑀 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
31 5 9 22 30 syl12anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 = ∅ ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
32 simpl2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ 𝑍 )
33 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
34 1 33 eqsstri ⊢ 𝑍 ⊆ ℤ
35 32 34 sstrdi ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ℤ )
36 simpr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
37 simpl3 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
38 zsupss ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
39 35 36 37 38 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
40 ssrexv ⊢ ( 𝐴 ⊆ 𝑍 → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
41 32 39 40 sylc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
42 31 41 pm2.61dane ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝑍 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝑍 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )