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