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 |
⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ∃ 𝑗 ∈ 𝑆 𝜑 ) → ∃ 𝑗 ∈ 𝑆 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) ) |