Proof of Theorem smfinfmpt
| Step | Hyp | Ref
| Expression |
| 1 | | smfinfmpt.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
| 2 | | smfinfmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 3 | | smfinfmpt.d |
. . . . 5
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} |
| 4 | | smfinfmpt.n |
. . . . . . . 8
⊢
Ⅎ𝑛𝜑 |
| 5 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))) |
| 6 | | smfinfmpt.f |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 7 | 5, 6 | fvmpt2d 7029 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 8 | 7 | dmeqd 5916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 9 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑍 |
| 10 | 9 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑛 ∈ 𝑍 |
| 11 | 2, 10 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 12 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 13 | | smfinfmpt.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 14 | 13 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 15 | 11, 12, 14 | dmmptdf 45229 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
| 16 | 8, 15 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐴 = dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 17 | 4, 16 | iineq2d 5015 |
. . . . . . 7
⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 𝐴 = ∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 18 | 2, 17 | rabeqd 3465 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵}) |
| 19 | | smfinfmpt.y |
. . . . . . . . 9
⊢
Ⅎ𝑦𝜑 |
| 20 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) |
| 21 | 19, 20 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 22 | | nfii1 5029 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) |
| 23 | 22 | nfcri 2897 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) |
| 24 | 4, 23 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 25 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 26 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 27 | | eliinid 45116 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 28 | 27 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) |
| 29 | 8, 15 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) = 𝐴) |
| 30 | 29 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) = 𝐴) |
| 31 | 28, 30 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ 𝐴) |
| 32 | 7 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 33 | 32 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 34 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 35 | | fvmpt4 45244 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 36 | 34, 13, 35 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 37 | 33, 36 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)) |
| 38 | 37 | breq2d 5155 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → (𝑦 ≤ 𝐵 ↔ 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 39 | 25, 26, 31, 38 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) ∧ 𝑛 ∈ 𝑍) → (𝑦 ≤ 𝐵 ↔ 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 40 | 24, 39 | ralbida 3270 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) → (∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵 ↔ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 41 | 21, 40 | rexbid 3274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 42 | 2, 41 | rabbida 3463 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)}) |
| 43 | 18, 42 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)}) |
| 44 | 3, 43 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)}) |
| 45 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛ℝ |
| 46 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵 |
| 47 | 45, 46 | nfrexw 3313 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵 |
| 48 | | nfii1 5029 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 𝐴 |
| 49 | 47, 48 | nfrabw 3475 |
. . . . . . . . . 10
⊢
Ⅎ𝑛{𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} |
| 50 | 3, 49 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐷 |
| 51 | 50 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ 𝐷 |
| 52 | 4, 51 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐷) |
| 53 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 54 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 55 | | rabidim1 3459 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵} → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴) |
| 56 | 55, 3 | eleq2s 2859 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 𝐴) |
| 57 | | eliinid 45116 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ 𝐴) |
| 58 | 56, 57 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ 𝐴) |
| 59 | 58 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ 𝐴) |
| 60 | 53, 54, 59, 37 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝐵 = (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)) |
| 61 | 52, 60 | mpteq2da 5240 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 62 | 61 | rneqd 5949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) = ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥))) |
| 63 | 62 | infeq1d 9517 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) = inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < )) |
| 64 | 2, 44, 63 | mpteq12da 5227 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} ↦ inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < ))) |
| 65 | 1, 64 | eqtrid 2789 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} ↦ inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < ))) |
| 66 | | nfmpt1 5250 |
. . 3
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 67 | | nfmpt1 5250 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 68 | 9, 67 | nfmpt 5249 |
. . 3
⊢
Ⅎ𝑥(𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 69 | | smfinfmpt.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 70 | | smfinfmpt.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 71 | | smfinfmpt.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 72 | 4, 6 | fmptd2f 45240 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)):𝑍⟶(SMblFn‘𝑆)) |
| 73 | | eqid 2737 |
. . 3
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} |
| 74 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} ↦ inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} ↦ inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < )) |
| 75 | 66, 68, 69, 70, 71, 72, 73, 74 | smfinf 46833 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom ((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)} ↦ inf(ran (𝑛 ∈ 𝑍 ↦ (((𝑛 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑛)‘𝑥)), ℝ, < )) ∈
(SMblFn‘𝑆)) |
| 76 | 65, 75 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |