| Step | Hyp | Ref
| Expression |
| 1 | | mbfsup.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
| 2 | 1 | anassrs 467 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 3 | 2 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 4 | 3 | fmpttd 7135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
| 5 | 4 | frnd 6744 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ) |
| 6 | | mbfsup.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 7 | | uzid 12893 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
| 9 | | mbfsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 10 | 8, 9 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
| 13 | 12, 3 | dmmptd 6713 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) = 𝑍) |
| 14 | 11, 13 | eleqtrrd 2844 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ dom (𝑛 ∈ 𝑍 ↦ 𝐵)) |
| 15 | 14 | ne0d 4342 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
| 16 | | dm0rn0 5935 |
. . . . . 6
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) = ∅) |
| 17 | 16 | necon3bii 2993 |
. . . . 5
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
| 18 | 15, 17 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
| 19 | | mbfsup.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦) |
| 20 | 4 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
| 21 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
| 22 | 21 | ralrn 7108 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
| 23 | 20, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
| 24 | | nffvmpt1 6917 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
| 25 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
≤ |
| 26 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑦 |
| 27 | 24, 25, 26 | nfbr 5190 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 |
| 28 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 |
| 29 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
| 30 | 29 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦)) |
| 31 | 27, 28, 30 | cbvralw 3306 |
. . . . . . . 8
⊢
(∀𝑚 ∈
𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦) |
| 32 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 33 | 12 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℝ) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
| 34 | 32, 3, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
| 35 | 34 | breq1d 5153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
| 36 | 35 | ralbidva 3176 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
| 37 | 31, 36 | bitrid 283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
| 38 | 23, 37 | bitrd 279 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
| 39 | 38 | rexbidv 3179 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
| 40 | 19, 39 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) |
| 41 | 5, 18, 40 | suprcld 12231 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 42 | | mbfsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
| 43 | 41, 42 | fmptd 7134 |
. 2
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
| 44 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 45 | | ltso 11341 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
| 46 | 45 | supex 9503 |
. . . . . . . . . . . . 13
⊢ sup(ran
(𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V |
| 47 | 42 | fvmpt2 7027 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
| 48 | 44, 46, 47 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
| 49 | 48 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))) |
| 50 | 5, 18, 40 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
| 52 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ ℝ) |
| 53 | | suprlub 12232 |
. . . . . . . . . . . 12
⊢ (((ran
(𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑡 ∈ ℝ) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
| 54 | 51, 52, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
| 55 | 20 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
| 56 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑡 < 𝑧 ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
| 57 | 56 | rexrn 7107 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
| 58 | 55, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
| 59 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑡 |
| 60 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
< |
| 61 | 59, 60, 24 | nfbr 5190 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
| 62 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) |
| 63 | 29 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛))) |
| 64 | 61, 62, 63 | cbvrexw 3307 |
. . . . . . . . . . . . 13
⊢
(∃𝑚 ∈
𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
| 65 | 12 | fvmpt2i 7026 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ( I ‘𝐵)) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 67 | 66 | fvmpt2i 7026 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
| 69 | 68 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( I ‘𝐵) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 70 | 65, 69 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 71 | 70 | breq2d 5155 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 72 | 71 | rexbidva 3177 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 73 | 72 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 74 | 64, 73 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 75 | 58, 74 | bitrd 279 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 76 | 49, 54, 75 | 3bitrd 305 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 77 | 76 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 78 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 79 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑡 |
| 80 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
< |
| 81 | | nfmpt1 5250 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
| 82 | 42, 81 | nfcxfr 2903 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐺 |
| 83 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑧 |
| 84 | 82, 83 | nffv 6916 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝐺‘𝑧) |
| 85 | 79, 80, 84 | nfbr 5190 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑡 < (𝐺‘𝑧) |
| 86 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑍 |
| 87 | | nffvmpt1 6917 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
| 88 | 79, 80, 87 | nfbr 5190 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
| 89 | 86, 88 | nfrexw 3313 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
| 90 | 85, 89 | nfbi 1903 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
| 91 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
| 92 | 91 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < (𝐺‘𝑧))) |
| 93 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
| 94 | 93 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 95 | 94 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 96 | 92, 95 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 97 | 78, 90, 96 | cbvralw 3306 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 98 | 77, 97 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 99 | 98 | r19.21bi 3251 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 100 | 43 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺:𝐴⟶ℝ) |
| 101 | 100 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) |
| 102 | | rexr 11307 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℝ*) |
| 103 | 102 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑡 ∈ ℝ*) |
| 104 | | elioopnf 13483 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ*
→ ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
| 105 | 103, 104 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
| 106 | 101, 105 | mpbirand 707 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < (𝐺‘𝑧))) |
| 107 | 103 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑡 ∈ ℝ*) |
| 108 | | elioopnf 13483 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ*
→ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 110 | 2 | fmpttd 7135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) |
| 111 | 110 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ) |
| 112 | 111 | biantrurd 532 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 113 | 112 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 114 | 113 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
| 115 | 109, 114 | bitr4d 282 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 116 | 115 | rexbidva 3177 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
| 117 | 99, 106, 116 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
| 118 | 117 | pm5.32da 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 119 | 43 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
| 120 | 119 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺 Fn 𝐴) |
| 121 | | elpreima 7078 |
. . . . . 6
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
| 122 | 120, 121 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
| 123 | | eliun 4995 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
| 124 | 110 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
| 125 | | elpreima 7078 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 126 | 124, 125 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 127 | 126 | rexbidva 3177 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 128 | 127 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 129 | | r19.42v 3191 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
| 130 | 128, 129 | bitrdi 287 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 131 | 123, 130 | bitrid 283 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
| 132 | 118, 122,
131 | 3bitr4d 311 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ 𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)))) |
| 133 | 132 | eqrdv 2735 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) = ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
| 134 | | zex 12622 |
. . . . . . 7
⊢ ℤ
∈ V |
| 135 | | uzssz 12899 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 136 | | ssdomg 9040 |
. . . . . . 7
⊢ (ℤ
∈ V → ((ℤ≥‘𝑀) ⊆ ℤ →
(ℤ≥‘𝑀) ≼ ℤ)) |
| 137 | 134, 135,
136 | mp2 9 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ≼ ℤ |
| 138 | 9, 137 | eqbrtri 5164 |
. . . . 5
⊢ 𝑍 ≼
ℤ |
| 139 | | znnen 16248 |
. . . . 5
⊢ ℤ
≈ ℕ |
| 140 | | domentr 9053 |
. . . . 5
⊢ ((𝑍 ≼ ℤ ∧ ℤ
≈ ℕ) → 𝑍
≼ ℕ) |
| 141 | 138, 139,
140 | mp2an 692 |
. . . 4
⊢ 𝑍 ≼
ℕ |
| 142 | | mbfsup.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
| 143 | | mbfima 25665 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 144 | 142, 110,
143 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 145 | 144 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 146 | 145 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 147 | | iunmbl2 25592 |
. . . 4
⊢ ((𝑍 ≼ ℕ ∧
∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 148 | 141, 146,
147 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
| 149 | 133, 148 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) ∈ dom
vol) |
| 150 | 43, 149 | ismbf3d 25689 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |