Step |
Hyp |
Ref |
Expression |
1 |
|
smflim.n |
⊢ Ⅎ 𝑚 𝐹 |
2 |
|
smflim.x |
⊢ Ⅎ 𝑥 𝐹 |
3 |
|
smflim.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
4 |
|
smflim.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
5 |
|
smflim.s |
⊢ ( 𝜑 → 𝑆 ∈ SAlg ) |
6 |
|
smflim.f |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) |
7 |
|
smflim.d |
⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
8 |
|
smflim.g |
⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) |
9 |
|
nfv |
⊢ Ⅎ 𝑎 𝜑 |
10 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑍 |
11 |
|
nfcv |
⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑛 ) |
12 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑚 |
13 |
2 12
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 ) |
14 |
13
|
nfdm |
⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 ) |
15 |
11 14
|
nfiin |
⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
16 |
10 15
|
nfiun |
⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
17 |
16
|
ssrab2f |
⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
18 |
7 17
|
eqsstri |
⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
19 |
18
|
a1i |
⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) |
20 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
21 |
4
|
eleq2i |
⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
22 |
21
|
biimpi |
⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
23 |
20 22
|
sseldi |
⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ ) |
24 |
|
uzid |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ) |
25 |
23 24
|
syl |
⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ) |
26 |
25
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ) |
27 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg ) |
28 |
6
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) ) |
29 |
|
eqid |
⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 ) |
30 |
27 28 29
|
smfdmss |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 ) |
31 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑛 |
32 |
1 31
|
nffv |
⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑛 ) |
33 |
32
|
nfdm |
⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 ) |
34 |
|
nfcv |
⊢ Ⅎ 𝑚 ∪ 𝑆 |
35 |
33 34
|
nfss |
⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 |
36 |
|
fveq2 |
⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) ) |
37 |
36
|
dmeqd |
⊢ ( 𝑚 = 𝑛 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑛 ) ) |
38 |
37
|
sseq1d |
⊢ ( 𝑚 = 𝑛 → ( dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ↔ dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 ) ) |
39 |
35 38
|
rspce |
⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ∧ dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ) |
40 |
26 30 39
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ) |
41 |
|
iinss |
⊢ ( ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ) |
42 |
40 41
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ) |
43 |
42
|
iunssd |
⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∪ 𝑆 ) |
44 |
19 43
|
sstrd |
⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 ) |
45 |
|
nfv |
⊢ Ⅎ 𝑚 𝜑 |
46 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑦 |
47 |
|
nfmpt1 |
⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
48 |
|
nfcv |
⊢ Ⅎ 𝑚 dom ⇝ |
49 |
47 48
|
nfel |
⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ |
50 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑍 |
51 |
|
nfii1 |
⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
52 |
50 51
|
nfiun |
⊢ Ⅎ 𝑚 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
53 |
49 52
|
nfrabw |
⊢ Ⅎ 𝑚 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
54 |
7 53
|
nfcxfr |
⊢ Ⅎ 𝑚 𝐷 |
55 |
46 54
|
nfel |
⊢ Ⅎ 𝑚 𝑦 ∈ 𝐷 |
56 |
45 55
|
nfan |
⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) |
57 |
|
nfcv |
⊢ Ⅎ 𝑤 𝐹 |
58 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg ) |
59 |
6
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) ) |
60 |
|
eqid |
⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 ) |
61 |
58 59 60
|
smff |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) |
62 |
61
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ ) |
63 |
|
nfcv |
⊢ Ⅎ 𝑦 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) |
64 |
|
nfv |
⊢ Ⅎ 𝑦 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ |
65 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑦 |
66 |
13 65
|
nffv |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) |
67 |
10 66
|
nfmpt |
⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) |
68 |
67
|
nfel1 |
⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ |
69 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) |
70 |
69
|
mpteq2dv |
⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) |
71 |
70
|
eleq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) ) |
72 |
16 63 64 68 71
|
cbvrabw |
⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ } |
73 |
|
nfcv |
⊢ Ⅎ 𝑙 dom ( 𝐹 ‘ 𝑚 ) |
74 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑙 |
75 |
1 74
|
nffv |
⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑙 ) |
76 |
75
|
nfdm |
⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑙 ) |
77 |
|
fveq2 |
⊢ ( 𝑚 = 𝑙 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑙 ) ) |
78 |
77
|
dmeqd |
⊢ ( 𝑚 = 𝑙 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑙 ) ) |
79 |
73 76 78
|
cbviin |
⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) |
80 |
79
|
a1i |
⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) ) |
81 |
|
fveq2 |
⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) ) |
82 |
|
eqidd |
⊢ ( ( 𝑛 = 𝑖 ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → dom ( 𝐹 ‘ 𝑙 ) = dom ( 𝐹 ‘ 𝑙 ) ) |
83 |
81 82
|
iineq12dv |
⊢ ( 𝑛 = 𝑖 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ) |
84 |
80 83
|
eqtrd |
⊢ ( 𝑛 = 𝑖 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ) |
85 |
84
|
cbviunv |
⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) |
86 |
85
|
eleq2i |
⊢ ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ) |
87 |
|
nfcv |
⊢ Ⅎ 𝑙 𝑍 |
88 |
|
nfcv |
⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) |
89 |
75 46
|
nffv |
⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) |
90 |
77
|
fveq1d |
⊢ ( 𝑚 = 𝑙 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) |
91 |
50 87 88 89 90
|
cbvmptf |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) |
92 |
91
|
eleq1i |
⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) |
93 |
86 92
|
anbi12i |
⊢ ( ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) ↔ ( 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∧ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) ) |
94 |
93
|
rabbia2 |
⊢ { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } |
95 |
7 72 94
|
3eqtri |
⊢ 𝐷 = { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } |
96 |
|
fveq2 |
⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) |
97 |
96
|
mpteq2dv |
⊢ ( 𝑦 = 𝑤 → ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ) |
98 |
97
|
eleq1d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) ) |
99 |
98
|
cbvrabv |
⊢ { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ } |
100 |
|
fveq2 |
⊢ ( 𝑙 = 𝑚 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑚 ) ) |
101 |
100
|
dmeqd |
⊢ ( 𝑙 = 𝑚 → dom ( 𝐹 ‘ 𝑙 ) = dom ( 𝐹 ‘ 𝑚 ) ) |
102 |
76 73 101
|
cbviin |
⊢ ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) |
103 |
102
|
a1i |
⊢ ( 𝑖 ∈ 𝑍 → ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
104 |
103
|
iuneq2i |
⊢ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) = ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) |
105 |
104
|
eleq2i |
⊢ ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ↔ 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ) |
106 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑤 |
107 |
75 106
|
nffv |
⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) |
108 |
|
nfcv |
⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) |
109 |
100
|
fveq1d |
⊢ ( 𝑙 = 𝑚 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) |
110 |
87 50 107 108 109
|
cbvmptf |
⊢ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) |
111 |
110
|
eleq1i |
⊢ ( ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) |
112 |
105 111
|
anbi12i |
⊢ ( ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∧ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) ↔ ( 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) ) |
113 |
112
|
rabbia2 |
⊢ { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑤 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ } |
114 |
99 113
|
eqtri |
⊢ { 𝑦 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑙 ) ∣ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ } |
115 |
95 114
|
eqtri |
⊢ 𝐷 = { 𝑤 ∈ ∪ 𝑖 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ∈ dom ⇝ } |
116 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 ) |
117 |
56 1 57 4 62 115 116
|
fnlimfvre |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ∈ ℝ ) |
118 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } |
119 |
7 118
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐷 |
120 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐷 |
121 |
|
nfcv |
⊢ Ⅎ 𝑦 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) |
122 |
|
nfcv |
⊢ Ⅎ 𝑥 ⇝ |
123 |
122 67
|
nffv |
⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) |
124 |
70
|
fveq2d |
⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
125 |
119 120 121 123 124
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
126 |
8 125
|
eqtri |
⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) ) |
127 |
117 126
|
fmptd |
⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ ) |
128 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℤ ) |
129 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg ) |
130 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) |
131 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑙 |
132 |
2 131
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑙 ) |
133 |
132 65
|
nffv |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) |
134 |
10 133
|
nfmpt |
⊢ Ⅎ 𝑥 ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) |
135 |
122 134
|
nffv |
⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) |
136 |
|
nfcv |
⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) |
137 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑥 |
138 |
75 137
|
nffv |
⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) |
139 |
77
|
fveq1d |
⊢ ( 𝑚 = 𝑙 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) |
140 |
50 87 136 138 139
|
cbvmptf |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) |
141 |
140
|
a1i |
⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) ) |
142 |
|
simpl |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍 ) → 𝑥 = 𝑦 ) |
143 |
142
|
fveq2d |
⊢ ( ( 𝑥 = 𝑦 ∧ 𝑙 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) |
144 |
143
|
mpteq2dva |
⊢ ( 𝑥 = 𝑦 → ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) |
145 |
141 144
|
eqtrd |
⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) |
146 |
145
|
fveq2d |
⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) ) |
147 |
119 120 121 135 146
|
cbvmptf |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) ) |
148 |
8 147
|
eqtri |
⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑙 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) ) ) ) |
149 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ ) |
150 |
|
nfcv |
⊢ Ⅎ 𝑚 < |
151 |
|
nfcv |
⊢ Ⅎ 𝑚 ( 𝑎 + ( 1 / 𝑗 ) ) |
152 |
89 150 151
|
nfbr |
⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) |
153 |
152 76
|
nfrabw |
⊢ Ⅎ 𝑚 { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } |
154 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑡 |
155 |
154 76
|
nfin |
⊢ Ⅎ 𝑚 ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) |
156 |
153 155
|
nfeq |
⊢ Ⅎ 𝑚 { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) |
157 |
|
nfcv |
⊢ Ⅎ 𝑚 𝑆 |
158 |
156 157
|
nfrabw |
⊢ Ⅎ 𝑚 { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } |
159 |
|
nfcv |
⊢ Ⅎ 𝑘 { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } |
160 |
|
nfcv |
⊢ Ⅎ 𝑙 { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } |
161 |
|
nfcv |
⊢ Ⅎ 𝑗 { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } |
162 |
|
nfcv |
⊢ Ⅎ 𝑦 dom ( 𝐹 ‘ 𝑙 ) |
163 |
132
|
nfdm |
⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑙 ) |
164 |
|
nfcv |
⊢ Ⅎ 𝑥 < |
165 |
|
nfcv |
⊢ Ⅎ 𝑥 ( 𝑎 + ( 1 / 𝑗 ) ) |
166 |
133 164 165
|
nfbr |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) |
167 |
|
nfv |
⊢ Ⅎ 𝑦 ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) |
168 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) ) |
169 |
168
|
breq1d |
⊢ ( 𝑦 = 𝑥 → ( ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ) |
170 |
162 163 166 167 169
|
cbvrabw |
⊢ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } |
171 |
170
|
a1i |
⊢ ( 𝑡 = 𝑠 → { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } ) |
172 |
|
ineq1 |
⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ) |
173 |
171 172
|
eqeq12d |
⊢ ( 𝑡 = 𝑠 → ( { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ) ) |
174 |
173
|
cbvrabv |
⊢ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } |
175 |
174
|
a1i |
⊢ ( 𝑙 = 𝑚 → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } ) |
176 |
101
|
eleq2d |
⊢ ( 𝑙 = 𝑚 → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ) |
177 |
100
|
fveq1d |
⊢ ( 𝑙 = 𝑚 → ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) |
178 |
177
|
breq1d |
⊢ ( 𝑙 = 𝑚 → ( ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ) |
179 |
176 178
|
anbi12d |
⊢ ( 𝑙 = 𝑚 → ( ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∧ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ↔ ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ) ) ) |
180 |
179
|
rabbidva2 |
⊢ ( 𝑙 = 𝑚 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } ) |
181 |
101
|
ineq2d |
⊢ ( 𝑙 = 𝑚 → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) |
182 |
180 181
|
eqeq12d |
⊢ ( 𝑙 = 𝑚 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) |
183 |
182
|
rabbidv |
⊢ ( 𝑙 = 𝑚 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
184 |
175 183
|
eqtrd |
⊢ ( 𝑙 = 𝑚 → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
185 |
|
oveq2 |
⊢ ( 𝑗 = 𝑘 → ( 1 / 𝑗 ) = ( 1 / 𝑘 ) ) |
186 |
185
|
oveq2d |
⊢ ( 𝑗 = 𝑘 → ( 𝑎 + ( 1 / 𝑗 ) ) = ( 𝑎 + ( 1 / 𝑘 ) ) ) |
187 |
186
|
breq2d |
⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) ) ) |
188 |
187
|
rabbidv |
⊢ ( 𝑗 = 𝑘 → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } ) |
189 |
188
|
eqeq1d |
⊢ ( 𝑗 = 𝑘 → ( { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ↔ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) ) |
190 |
189
|
rabbidv |
⊢ ( 𝑗 = 𝑘 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
191 |
184 190
|
sylan9eq |
⊢ ( ( 𝑙 = 𝑚 ∧ 𝑗 = 𝑘 ) → { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
192 |
158 159 160 161 191
|
cbvmpo |
⊢ ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } ) = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) |
193 |
192
|
eqcomi |
⊢ ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝑎 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ) = ( 𝑙 ∈ 𝑍 , 𝑗 ∈ ℕ ↦ { 𝑡 ∈ 𝑆 ∣ { 𝑦 ∈ dom ( 𝐹 ‘ 𝑙 ) ∣ ( ( 𝐹 ‘ 𝑙 ) ‘ 𝑦 ) < ( 𝑎 + ( 1 / 𝑗 ) ) } = ( 𝑡 ∩ dom ( 𝐹 ‘ 𝑙 ) ) } ) |
194 |
128 4 129 130 95 148 149 193
|
smflimlem6 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐺 ‘ 𝑦 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) |
195 |
9 5 44 127 194
|
issmfled |
⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) ) |