Step |
Hyp |
Ref |
Expression |
1 |
|
smflimlem2.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
smflimlem2.2 |
⊢ ( 𝜑 → 𝑆 ∈ SAlg ) |
3 |
|
smflimlem2.3 |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) |
4 |
|
smflimlem2.4 |
⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
5 |
|
smflimlem2.5 |
⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
6 |
|
smflimlem2.6 |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
7 |
|
smflimlem2.7 |
⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
8 |
|
smflimlem2.8 |
⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) |
9 |
|
smflimlem2.9 |
⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) |
10 |
|
smflimlem2.10 |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) |
11 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
12 |
4 11
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐷 |
13 |
12
|
ssrab2f |
⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷 |
14 |
13
|
a1i |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐷 ) |
15 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ 𝐷 ) |
16 |
|
ssrab2 |
⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
17 |
4 16
|
eqsstri |
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
18 |
17
|
sseli |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) |
19 |
|
fveq2 |
⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) ) |
20 |
19
|
iineq1d |
⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
21 |
20
|
cbviunv |
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) |
22 |
21
|
eleq2i |
⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
23 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
24 |
22 23
|
bitri |
⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
25 |
18 24
|
sylib |
⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
26 |
15 25
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
27 |
|
nfv |
⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) |
28 |
|
nfv |
⊢ Ⅎ 𝑚 𝑘 ∈ ℕ |
29 |
27 28
|
nfan |
⊢ Ⅎ 𝑚 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) |
30 |
|
nfv |
⊢ Ⅎ 𝑚 𝑖 ∈ 𝑍 |
31 |
29 30
|
nfan |
⊢ Ⅎ 𝑚 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) |
32 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑥 |
33 |
|
nfii1 |
⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) |
34 |
32 33
|
nfel |
⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) |
35 |
31 34
|
nfan |
⊢ Ⅎ 𝑚 ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
36 |
|
nfmpt1 |
⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
37 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑖 ) |
38 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
39 |
1
|
eleq2i |
⊢ ( 𝑖 ∈ 𝑍 ↔ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
40 |
39
|
biimpi |
⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
41 |
38 40
|
sseldi |
⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ ) |
42 |
|
uzid |
⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
43 |
41 42
|
syl |
⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
44 |
43
|
ad2antlr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
45 |
|
simplll |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ) |
46 |
45
|
simpld |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 ) |
47 |
|
uzss |
⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
48 |
40 47
|
syl |
⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
49 |
48 1
|
sseqtrrdi |
⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 ) |
50 |
49
|
sselda |
⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 ) |
51 |
50
|
ad4ant24 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑚 ∈ 𝑍 ) |
52 |
|
eliinid |
⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) |
53 |
52
|
adantll |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) |
54 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) |
55 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V ) |
56 |
54 55
|
fvmpt2d |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
57 |
56
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
58 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg ) |
59 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) ) |
60 |
|
eqid |
⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 ) |
61 |
58 59 60
|
smff |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) |
62 |
61
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) |
63 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) |
64 |
62 63
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ ) |
65 |
57 64
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ) |
66 |
46 51 53 65
|
syl3anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ) |
67 |
66
|
adantl3r |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ) |
68 |
67
|
adantl3r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ) |
69 |
4
|
eleq2i |
⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) |
70 |
69
|
biimpi |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) |
71 |
|
rabidim2 |
⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) |
72 |
70 71
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) |
73 |
|
climdm |
⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
74 |
72 73
|
sylib |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
75 |
74
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
76 |
75 73
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) |
77 |
76 73
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
78 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐹 |
79 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 ) |
80 |
12 78 5 79
|
fnlimfv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑥 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
81 |
80
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝑥 ) ) |
82 |
77 81
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) |
83 |
82
|
ad4antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ) |
84 |
6
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝐴 ∈ ℝ ) |
85 |
|
simp-4r |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) |
86 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑘 ∈ ℕ ) |
87 |
|
nnrecrp |
⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ ) |
88 |
86 87
|
syl |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 1 / 𝑘 ) ∈ ℝ+ ) |
89 |
35 36 37 44 68 83 84 85 88
|
climleltrp |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) |
90 |
|
simp-6l |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 ) |
91 |
|
simplr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑖 ∈ 𝑍 ) |
92 |
91
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑖 ∈ 𝑍 ) |
93 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
94 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
95 |
|
nfv |
⊢ Ⅎ 𝑚 𝜑 |
96 |
95 30 34
|
nf3an |
⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
97 |
|
nfv |
⊢ Ⅎ 𝑚 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) |
98 |
96 97
|
nfan |
⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
99 |
|
simpll |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ) |
100 |
37
|
uztrn2 |
⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
101 |
100
|
adantll |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
102 |
|
simpll2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑖 ∈ 𝑍 ) |
103 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
104 |
102 103 50
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑚 ∈ 𝑍 ) |
105 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) |
106 |
|
id |
⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍 ) |
107 |
|
fvexd |
⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V ) |
108 |
|
eqid |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
109 |
108
|
fvmpt2 |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
110 |
106 107 109
|
syl2anc |
⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
111 |
110
|
eqcomd |
⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ) |
112 |
111
|
adantr |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ) |
113 |
|
simpr |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) |
114 |
112 113
|
eqbrtrd |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) |
115 |
104 105 114
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) |
116 |
52
|
3ad2antl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) |
117 |
116
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) |
118 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) |
119 |
117 118
|
jca |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) |
120 |
|
rabid |
⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) |
121 |
119 120
|
sylibr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
122 |
115 121
|
syldan |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
123 |
122
|
adantrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
124 |
123
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
125 |
99 101 124
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
126 |
98 125
|
ralimdaa |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
127 |
90 92 93 94 126
|
syl31anc |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
128 |
127
|
reximdva |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ‘ 𝑚 ) < ( 𝐴 + ( 1 / 𝑘 ) ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
129 |
89 128
|
mpd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
130 |
|
ssrexv |
⊢ ( ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
131 |
49 130
|
syl |
⊢ ( 𝑖 ∈ 𝑍 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
132 |
131
|
ad2antlr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
133 |
129 132
|
mpd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
134 |
133
|
rexlimdva2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑖 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ) |
135 |
26 134
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
136 |
|
nfv |
⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) |
137 |
|
nfra1 |
⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } |
138 |
136 137
|
nfan |
⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
139 |
|
simpll1 |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 ) |
140 |
|
simpll2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ ) |
141 |
1
|
uztrn2 |
⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 ) |
142 |
141
|
ssd |
⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 ) |
143 |
142
|
sselda |
⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 ) |
144 |
143
|
adantll |
⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 ) |
145 |
144
|
3adantl1 |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 ) |
146 |
145
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 ) |
147 |
|
rspa |
⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
148 |
147
|
adantll |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
149 |
|
simp1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝜑 ) |
150 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 ) |
151 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑘 ∈ ℕ ) |
152 |
|
eqid |
⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } |
153 |
152 2
|
rabexd |
⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) |
154 |
153
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) |
155 |
154
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) |
156 |
155
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) |
157 |
7
|
elrnmpoid |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) |
158 |
150 151 156 157
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) |
159 |
|
ovex |
⊢ ( 𝑚 𝑃 𝑘 ) ∈ V |
160 |
|
eleq1 |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝑟 ∈ ran 𝑃 ↔ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) ) |
161 |
160
|
anbi2d |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) ↔ ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) ) ) |
162 |
|
fveq2 |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝐶 ‘ 𝑟 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) |
163 |
|
id |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → 𝑟 = ( 𝑚 𝑃 𝑘 ) ) |
164 |
162 163
|
eleq12d |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ↔ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) ) |
165 |
161 164
|
imbi12d |
⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) ↔ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) ) ) |
166 |
159 165 10
|
vtocl |
⊢ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) |
167 |
149 158 166
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) |
168 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V ) |
169 |
8
|
ovmpt4g |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) |
170 |
150 151 168 169
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ) |
171 |
170
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) = ( 𝑚 𝐻 𝑘 ) ) |
172 |
149 153
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) |
173 |
7
|
ovmpt4g |
⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
174 |
150 151 172 173
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
175 |
171 174
|
eleq12d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ↔ ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) ) |
176 |
167 175
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
177 |
|
ineq1 |
⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) |
178 |
177
|
eqeq2d |
⊢ ( 𝑠 = ( 𝑚 𝐻 𝑘 ) → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) |
179 |
178
|
elrab |
⊢ ( ( 𝑚 𝐻 𝑘 ) ∈ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ↔ ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) |
180 |
176 179
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 ∧ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) |
181 |
180
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) |
182 |
|
inss1 |
⊢ ( ( 𝑚 𝐻 𝑘 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ⊆ ( 𝑚 𝐻 𝑘 ) |
183 |
181 182
|
eqsstrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) ) |
184 |
183
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ⊆ ( 𝑚 𝐻 𝑘 ) ) |
185 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) |
186 |
184 185
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) |
187 |
139 140 146 148 186
|
syl31anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) |
188 |
187
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) ) |
189 |
138 188
|
ralrimi |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) |
190 |
|
vex |
⊢ 𝑥 ∈ V |
191 |
|
eliin |
⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) ) |
192 |
190 191
|
ax-mp |
⊢ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ ( 𝑚 𝐻 𝑘 ) ) |
193 |
189 192
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
194 |
193
|
ex |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) ) |
195 |
194
|
ad5ant145 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) ) |
196 |
195
|
reximdva |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) ) |
197 |
135 196
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
198 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
199 |
197 198
|
sylibr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
200 |
199
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
201 |
|
eliin |
⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) ) |
202 |
190 201
|
ax-mp |
⊢ ( 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
203 |
200 202
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ) |
204 |
203 9
|
eleqtrrdi |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 ) → 𝑥 ∈ 𝐼 ) |
205 |
204
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) ) |
206 |
205
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) ) |
207 |
|
rabss |
⊢ ( { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 → 𝑥 ∈ 𝐼 ) ) |
208 |
206 207
|
sylibr |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ 𝐼 ) |
209 |
14 208
|
ssind |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑥 ) ≤ 𝐴 } ⊆ ( 𝐷 ∩ 𝐼 ) ) |