This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzwo4

Description: Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses uzwo4.1 ⊢ Ⅎ 𝑗 𝜓
uzwo4.2 ⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜓 ) )
Assertion uzwo4 ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 uzwo4.1 ⊢ Ⅎ 𝑗 𝜓
2 uzwo4.2 ⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜓 ) )
3 ssrab2 ⊢ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ⊆ 𝑆
4 3 a1i ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → { 𝑗 ∈ 𝑆 ∣ 𝜑 } ⊆ 𝑆 )
5 id ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) )
6 4 5 sstrd ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → { 𝑗 ∈ 𝑆 ∣ 𝜑 } ⊆ ( ℤ≥ ‘ 𝑀 ) )
7 6 adantr ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → { 𝑗 ∈ 𝑆 ∣ 𝜑 } ⊆ ( ℤ≥ ‘ 𝑀 ) )
8 rabn0 ⊢ ( { 𝑗 ∈ 𝑆 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑗 ∈ 𝑆 𝜑 )
9 8 bicomi ⊢ ( ∃ 𝑗 ∈ 𝑆 𝜑 ↔ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ≠ ∅ )
10 9 biimpi ⊢ ( ∃ 𝑗 ∈ 𝑆 𝜑 → { 𝑗 ∈ 𝑆 ∣ 𝜑 } ≠ ∅ )
11 10 adantl ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → { 𝑗 ∈ 𝑆 ∣ 𝜑 } ≠ ∅ )
12 uzwo ⊢ ( ( { 𝑗 ∈ 𝑆 ∣ 𝜑 } ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ≠ ∅ ) → ∃ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 )
13 7 11 12 syl2anc ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → ∃ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 )
14 3 sseli ⊢ ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } → 𝑖 ∈ 𝑆 )
15 14 adantr ⊢ ( ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → 𝑖 ∈ 𝑆 )
16 15 3adant1 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → 𝑖 ∈ 𝑆 )
17 nfcv ⊢ Ⅎ 𝑗 𝑖
18 nfcv ⊢ Ⅎ 𝑗 𝑆
19 17 nfsbc1 ⊢ Ⅎ 𝑗 [ 𝑖 / 𝑗 ] 𝜑
20 sbceq1a ⊢ ( 𝑗 = 𝑖 → ( 𝜑 ↔ [ 𝑖 / 𝑗 ] 𝜑 ) )
21 17 18 19 20 elrabf ⊢ ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ↔ ( 𝑖 ∈ 𝑆 ∧ [ 𝑖 / 𝑗 ] 𝜑 ) )
22 21 biimpi ⊢ ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } → ( 𝑖 ∈ 𝑆 ∧ [ 𝑖 / 𝑗 ] 𝜑 ) )
23 22 simprd ⊢ ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } → [ 𝑖 / 𝑗 ] 𝜑 )
24 23 adantr ⊢ ( ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → [ 𝑖 / 𝑗 ] 𝜑 )
25 24 3adant1 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → [ 𝑖 / 𝑗 ] 𝜑 )
26 nfv ⊢ Ⅎ 𝑘 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 )
27 nfv ⊢ Ⅎ 𝑘 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 }
28 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘
29 26 27 28 nf3an ⊢ Ⅎ 𝑘 ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 )
30 simpl13 ⊢ ( ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) ∧ 𝜓 ) → ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 )
31 simpl2 ⊢ ( ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) ∧ 𝜓 ) → 𝑘 ∈ 𝑆 )
32 simpr ⊢ ( ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) ∧ 𝜓 ) → 𝜓 )
33 simpll ⊢ ( ( ( ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝜓 ) → ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 )
34 id ⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑆 ∧ 𝜓 ) )
35 nfcv ⊢ Ⅎ 𝑗 𝑘
36 35 18 1 2 elrabf ⊢ ( 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ↔ ( 𝑘 ∈ 𝑆 ∧ 𝜓 ) )
37 34 36 sylibr ⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝜓 ) → 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } )
38 37 adantll ⊢ ( ( ( ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝜓 ) → 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } )
39 rspa ⊢ ( ( ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ∧ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ) → 𝑖 ≤ 𝑘 )
40 33 38 39 syl2anc ⊢ ( ( ( ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ∧ 𝑘 ∈ 𝑆 ) ∧ 𝜓 ) → 𝑖 ≤ 𝑘 )
41 30 31 32 40 syl21anc ⊢ ( ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) ∧ 𝜓 ) → 𝑖 ≤ 𝑘 )
42 6 sselda ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
43 eluzelz ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑖 ∈ ℤ )
44 42 43 syl ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ) → 𝑖 ∈ ℤ )
45 44 zred ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ) → 𝑖 ∈ ℝ )
46 45 3adant3 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → 𝑖 ∈ ℝ )
47 46 3ad2ant1 ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) → 𝑖 ∈ ℝ )
48 ssel2 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
49 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
50 48 49 syl ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ ℤ )
51 50 zred ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ ℝ )
52 51 3ad2antl1 ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ ℝ )
53 52 3adant3 ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) → 𝑘 ∈ ℝ )
54 simp3 ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) → 𝑘 < 𝑖 )
55 simp3 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑘 < 𝑖 ) → 𝑘 < 𝑖 )
56 simp2 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑘 < 𝑖 ) → 𝑘 ∈ ℝ )
57 simp1 ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑘 < 𝑖 ) → 𝑖 ∈ ℝ )
58 56 57 ltnled ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑘 < 𝑖 ) → ( 𝑘 < 𝑖 ↔ ¬ 𝑖 ≤ 𝑘 ) )
59 55 58 mpbid ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑘 < 𝑖 ) → ¬ 𝑖 ≤ 𝑘 )
60 47 53 54 59 syl3anc ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) → ¬ 𝑖 ≤ 𝑘 )
61 60 adantr ⊢ ( ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) ∧ 𝜓 ) → ¬ 𝑖 ≤ 𝑘 )
62 41 61 pm2.65da ⊢ ( ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) ∧ 𝑘 ∈ 𝑆 ∧ 𝑘 < 𝑖 ) → ¬ 𝜓 )
63 62 3exp ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → ( 𝑘 ∈ 𝑆 → ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) )
64 29 63 ralrimi ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) )
65 25 64 jca ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → ( [ 𝑖 / 𝑗 ] 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) )
66 nfv ⊢ Ⅎ 𝑗 𝑘 < 𝑖
67 1 nfn ⊢ Ⅎ 𝑗 ¬ 𝜓
68 66 67 nfim ⊢ Ⅎ 𝑗 ( 𝑘 < 𝑖 → ¬ 𝜓 )
69 18 68 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 )
70 19 69 nfan ⊢ Ⅎ 𝑗 ( [ 𝑖 / 𝑗 ] 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) )
71 breq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑘 < 𝑗 ↔ 𝑘 < 𝑖 ) )
72 71 imbi1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑘 < 𝑗 → ¬ 𝜓 ) ↔ ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) )
73 72 ralbidv ⊢ ( 𝑗 = 𝑖 → ( ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ↔ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) )
74 20 73 anbi12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) ↔ ( [ 𝑖 / 𝑗 ] 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) ) )
75 70 74 rspce ⊢ ( ( 𝑖 ∈ 𝑆 ∧ ( [ 𝑖 / 𝑗 ] 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑖 → ¬ 𝜓 ) ) ) → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) )
76 16 65 75 syl2anc ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 ) → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) )
77 76 3exp ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } → ( ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) ) ) )
78 77 rexlimdv ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → ( ∃ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) ) )
79 78 adantr ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → ( ∃ 𝑖 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } ∀ 𝑘 ∈ { 𝑗 ∈ 𝑆 ∣ 𝜑 } 𝑖 ≤ 𝑘 → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) ) )
80 13 79 mpd ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) )