| Step | Hyp | Ref
| Expression |
| 1 | | smfsup.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 2 | | smfsup.z |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | | smfsup.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 4 | | smfsup.f |
. 2
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 5 | | smfsup.d |
. . 3
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
| 6 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑤∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 7 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥𝑍 |
| 8 | | smfsup.x |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
| 9 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑚 |
| 10 | 8, 9 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥(𝐹‘𝑚) |
| 11 | 10 | nfdm 5962 |
. . . . 5
⊢
Ⅎ𝑥dom
(𝐹‘𝑚) |
| 12 | 7, 11 | nfiin 5024 |
. . . 4
⊢
Ⅎ𝑥∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚) |
| 13 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑤∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 |
| 14 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥ℝ |
| 15 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑤 |
| 16 | 10, 15 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑤) |
| 17 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥
≤ |
| 18 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑧 |
| 19 | 16, 17, 18 | nfbr 5190 |
. . . . . 6
⊢
Ⅎ𝑥((𝐹‘𝑚)‘𝑤) ≤ 𝑧 |
| 20 | 7, 19 | nfralw 3311 |
. . . . 5
⊢
Ⅎ𝑥∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧 |
| 21 | 14, 20 | nfrexw 3313 |
. . . 4
⊢
Ⅎ𝑥∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧 |
| 22 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑚dom
(𝐹‘𝑛) |
| 23 | | smfsup.n |
. . . . . . . 8
⊢
Ⅎ𝑛𝐹 |
| 24 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛𝑚 |
| 25 | 23, 24 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑛(𝐹‘𝑚) |
| 26 | 25 | nfdm 5962 |
. . . . . 6
⊢
Ⅎ𝑛dom
(𝐹‘𝑚) |
| 27 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
| 28 | 27 | dmeqd 5916 |
. . . . . 6
⊢ (𝑛 = 𝑚 → dom (𝐹‘𝑛) = dom (𝐹‘𝑚)) |
| 29 | 22, 26, 28 | cbviin 5037 |
. . . . 5
⊢ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚) |
| 30 | 29 | a1i 11 |
. . . 4
⊢ (𝑥 = 𝑤 → ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚)) |
| 31 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑤)) |
| 32 | 31 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑛)‘𝑤) ≤ 𝑦)) |
| 33 | 32 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦)) |
| 34 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑛)‘𝑤) ≤ 𝑦 |
| 35 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛𝑤 |
| 36 | 25, 35 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((𝐹‘𝑚)‘𝑤) |
| 37 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
≤ |
| 38 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑦 |
| 39 | 36, 37, 38 | nfbr 5190 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝐹‘𝑚)‘𝑤) ≤ 𝑦 |
| 40 | 27 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) |
| 41 | 40 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) |
| 42 | 34, 39, 41 | cbvralw 3306 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦) |
| 43 | 42 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) |
| 44 | 33, 43 | bitrd 279 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) |
| 45 | 44 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) |
| 46 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (((𝐹‘𝑚)‘𝑤) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑤) ≤ 𝑧)) |
| 47 | 46 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧)) |
| 48 | 47 | cbvrexvw 3238 |
. . . . . 6
⊢
(∃𝑦 ∈
ℝ ∀𝑚 ∈
𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦 ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧) |
| 49 | 48 | a1i 11 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦 ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧)) |
| 50 | 45, 49 | bitrd 279 |
. . . 4
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧)) |
| 51 | 6, 12, 13, 21, 30, 50 | cbvrabcsfw 3940 |
. . 3
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧} |
| 52 | 5, 51 | eqtri 2765 |
. 2
⊢ 𝐷 = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑧} |
| 53 | | smfsup.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 54 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
| 55 | 5, 54 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑥𝐷 |
| 56 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑤𝐷 |
| 57 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑤sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) |
| 58 | 7, 16 | nfmpt 5249 |
. . . . . 6
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) |
| 59 | 58 | nfrn 5963 |
. . . . 5
⊢
Ⅎ𝑥ran
(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) |
| 60 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥
< |
| 61 | 59, 14, 60 | nfsup 9491 |
. . . 4
⊢
Ⅎ𝑥sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < ) |
| 62 | 31 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) |
| 63 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝐹‘𝑛)‘𝑤) |
| 64 | 63, 36, 40 | cbvmpt 5253 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) |
| 65 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) |
| 66 | 62, 65 | eqtrd 2777 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) |
| 67 | 66 | rneqd 5949 |
. . . . 5
⊢ (𝑥 = 𝑤 → ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) |
| 68 | 67 | supeq1d 9486 |
. . . 4
⊢ (𝑥 = 𝑤 → sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) |
| 69 | 55, 56, 57, 61, 68 | cbvmptf 5251 |
. . 3
⊢ (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑤 ∈ 𝐷 ↦ sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) |
| 70 | 53, 69 | eqtri 2765 |
. 2
⊢ 𝐺 = (𝑤 ∈ 𝐷 ↦ sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) |
| 71 | 1, 2, 3, 4, 52, 70 | smfsuplem3 46828 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |