Metamath Proof Explorer

Theorem uzwo

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005)

Ref Expression
Assertion uzwo ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( ℎ = 𝑀 → ( ℎ ≤ 𝑡 ↔ 𝑀 ≤ 𝑡 ) )
2 1 ralbidv ⊢ ( ℎ = 𝑀 → ( ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 𝑀 ≤ 𝑡 ) )
3 2 imbi2d ⊢ ( ℎ = 𝑀 → ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ) ↔ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑀 ≤ 𝑡 ) ) )
4 breq1 ⊢ ( ℎ = 𝑚 → ( ℎ ≤ 𝑡 ↔ 𝑚 ≤ 𝑡 ) )
5 4 ralbidv ⊢ ( ℎ = 𝑚 → ( ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 ) )
6 5 imbi2d ⊢ ( ℎ = 𝑚 → ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ) ↔ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 ) ) )
7 breq1 ⊢ ( ℎ = ( 𝑚 + 1 ) → ( ℎ ≤ 𝑡 ↔ ( 𝑚 + 1 ) ≤ 𝑡 ) )
8 7 ralbidv ⊢ ( ℎ = ( 𝑚 + 1 ) → ( ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) )
9 8 imbi2d ⊢ ( ℎ = ( 𝑚 + 1 ) → ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ) ↔ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
10 breq1 ⊢ ( ℎ = 𝑛 → ( ℎ ≤ 𝑡 ↔ 𝑛 ≤ 𝑡 ) )
11 10 ralbidv ⊢ ( ℎ = 𝑛 → ( ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 ) )
12 11 imbi2d ⊢ ( ℎ = 𝑛 → ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ℎ ≤ 𝑡 ) ↔ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 ) ) )
13 ssel ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( 𝑡 ∈ 𝑆 → 𝑡 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
14 eluzle ⊢ ( 𝑡 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑡 )
15 13 14 syl6 ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( 𝑡 ∈ 𝑆 → 𝑀 ≤ 𝑡 ) )
16 15 ralrimiv ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ∀ 𝑡 ∈ 𝑆 𝑀 ≤ 𝑡 )
17 16 adantr ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑀 ≤ 𝑡 )
18 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
19 sstr ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ ) → 𝑆 ⊆ ℤ )
20 18 19 mpan2 ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → 𝑆 ⊆ ℤ )
21 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑚 ∈ ℤ )
22 breq1 ⊢ ( 𝑗 = 𝑚 → ( 𝑗 ≤ 𝑡 ↔ 𝑚 ≤ 𝑡 ) )
23 22 ralbidv ⊢ ( 𝑗 = 𝑚 → ( ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 ) )
24 23 rspcev ⊢ ( ( 𝑚 ∈ 𝑆 ∧ ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 )
25 24 expcom ⊢ ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ( 𝑚 ∈ 𝑆 → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) )
26 25 con3rr3 ⊢ ( ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ¬ 𝑚 ∈ 𝑆 ) )
27 ssel2 ⊢ ( ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) → 𝑡 ∈ ℤ )
28 zre ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℝ )
29 zre ⊢ ( 𝑡 ∈ ℤ → 𝑡 ∈ ℝ )
30 letri3 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑚 = 𝑡 ↔ ( 𝑚 ≤ 𝑡 ∧ 𝑡 ≤ 𝑚 ) ) )
31 28 29 30 syl2an ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝑚 = 𝑡 ↔ ( 𝑚 ≤ 𝑡 ∧ 𝑡 ≤ 𝑚 ) ) )
32 zleltp1 ⊢ ( ( 𝑡 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑡 ≤ 𝑚 ↔ 𝑡 < ( 𝑚 + 1 ) ) )
33 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
34 28 33 syl ⊢ ( 𝑚 ∈ ℤ → ( 𝑚 + 1 ) ∈ ℝ )
35 ltnle ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑚 + 1 ) ∈ ℝ ) → ( 𝑡 < ( 𝑚 + 1 ) ↔ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) )
36 29 34 35 syl2an ⊢ ( ( 𝑡 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑡 < ( 𝑚 + 1 ) ↔ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) )
37 32 36 bitrd ⊢ ( ( 𝑡 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑡 ≤ 𝑚 ↔ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) )
38 37 ancoms ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝑡 ≤ 𝑚 ↔ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) )
39 38 anbi2d ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( ( 𝑚 ≤ 𝑡 ∧ 𝑡 ≤ 𝑚 ) ↔ ( 𝑚 ≤ 𝑡 ∧ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
40 31 39 bitrd ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝑚 = 𝑡 ↔ ( 𝑚 ≤ 𝑡 ∧ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
41 27 40 sylan2 ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( 𝑚 = 𝑡 ↔ ( 𝑚 ≤ 𝑡 ∧ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
42 eleq1a ⊢ ( 𝑡 ∈ 𝑆 → ( 𝑚 = 𝑡 → 𝑚 ∈ 𝑆 ) )
43 42 ad2antll ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( 𝑚 = 𝑡 → 𝑚 ∈ 𝑆 ) )
44 41 43 sylbird ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( ( 𝑚 ≤ 𝑡 ∧ ¬ ( 𝑚 + 1 ) ≤ 𝑡 ) → 𝑚 ∈ 𝑆 ) )
45 44 expd ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( 𝑚 ≤ 𝑡 → ( ¬ ( 𝑚 + 1 ) ≤ 𝑡 → 𝑚 ∈ 𝑆 ) ) )
46 con1 ⊢ ( ( ¬ ( 𝑚 + 1 ) ≤ 𝑡 → 𝑚 ∈ 𝑆 ) → ( ¬ 𝑚 ∈ 𝑆 → ( 𝑚 + 1 ) ≤ 𝑡 ) )
47 45 46 syl6 ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( 𝑚 ≤ 𝑡 → ( ¬ 𝑚 ∈ 𝑆 → ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
48 47 com23 ⊢ ( ( 𝑚 ∈ ℤ ∧ ( 𝑆 ⊆ ℤ ∧ 𝑡 ∈ 𝑆 ) ) → ( ¬ 𝑚 ∈ 𝑆 → ( 𝑚 ≤ 𝑡 → ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
49 48 exp32 ⊢ ( 𝑚 ∈ ℤ → ( 𝑆 ⊆ ℤ → ( 𝑡 ∈ 𝑆 → ( ¬ 𝑚 ∈ 𝑆 → ( 𝑚 ≤ 𝑡 → ( 𝑚 + 1 ) ≤ 𝑡 ) ) ) ) )
50 49 com34 ⊢ ( 𝑚 ∈ ℤ → ( 𝑆 ⊆ ℤ → ( ¬ 𝑚 ∈ 𝑆 → ( 𝑡 ∈ 𝑆 → ( 𝑚 ≤ 𝑡 → ( 𝑚 + 1 ) ≤ 𝑡 ) ) ) ) )
51 50 imp41 ⊢ ( ( ( ( 𝑚 ∈ ℤ ∧ 𝑆 ⊆ ℤ ) ∧ ¬ 𝑚 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑆 ) → ( 𝑚 ≤ 𝑡 → ( 𝑚 + 1 ) ≤ 𝑡 ) )
52 51 ralimdva ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑆 ⊆ ℤ ) ∧ ¬ 𝑚 ∈ 𝑆 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) )
53 52 ex ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑆 ⊆ ℤ ) → ( ¬ 𝑚 ∈ 𝑆 → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
54 26 53 sylan9r ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑆 ⊆ ℤ ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
55 54 pm2.43d ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑆 ⊆ ℤ ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) )
56 55 expl ⊢ ( 𝑚 ∈ ℤ → ( ( 𝑆 ⊆ ℤ ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
57 21 56 syl ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑆 ⊆ ℤ ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
58 20 57 sylani ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
59 58 a2d ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑚 ≤ 𝑡 ) → ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 ( 𝑚 + 1 ) ≤ 𝑡 ) ) )
60 3 6 9 12 17 59 uzind4i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 ) )
61 breq1 ⊢ ( 𝑗 = 𝑛 → ( 𝑗 ≤ 𝑡 ↔ 𝑛 ≤ 𝑡 ) )
62 61 ralbidv ⊢ ( 𝑗 = 𝑛 → ( ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ↔ ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 ) )
63 62 rspcev ⊢ ( ( 𝑛 ∈ 𝑆 ∧ ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 )
64 63 expcom ⊢ ( ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 → ( 𝑛 ∈ 𝑆 → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) )
65 64 con3rr3 ⊢ ( ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 → ( ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 → ¬ 𝑛 ∈ 𝑆 ) )
66 65 adantl ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ( ∀ 𝑡 ∈ 𝑆 𝑛 ≤ 𝑡 → ¬ 𝑛 ∈ 𝑆 ) )
67 60 66 sylcom ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ¬ 𝑛 ∈ 𝑆 ) )
68 ssel ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 ∈ 𝑆 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
69 68 con3rr3 ⊢ ( ¬ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ¬ 𝑛 ∈ 𝑆 ) )
70 69 adantrd ⊢ ( ¬ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ¬ 𝑛 ∈ 𝑆 ) )
71 67 70 pm2.61i ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) → ¬ 𝑛 ∈ 𝑆 )
72 71 ex ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 → ¬ 𝑛 ∈ 𝑆 ) )
73 72 alrimdv ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 → ∀ 𝑛 ¬ 𝑛 ∈ 𝑆 ) )
74 eq0 ⊢ ( 𝑆 = ∅ ↔ ∀ 𝑛 ¬ 𝑛 ∈ 𝑆 )
75 73 74 syl6ibr ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( ¬ ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 → 𝑆 = ∅ ) )
76 75 necon1ad ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( 𝑆 ≠ ∅ → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ) )
77 76 imp ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 )
78 breq2 ⊢ ( 𝑡 = 𝑘 → ( 𝑗 ≤ 𝑡 ↔ 𝑗 ≤ 𝑘 ) )
79 78 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ↔ ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
80 79 rexbii ⊢ ( ∃ 𝑗 ∈ 𝑆 ∀ 𝑡 ∈ 𝑆 𝑗 ≤ 𝑡 ↔ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
81 77 80 sylib ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )