Step | Hyp | Ref
| Expression |
1 | | mbfsup.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
2 | 1 | anassrs 471 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
3 | 2 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
4 | 3 | fmpttd 6937 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
5 | 4 | frnd 6558 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ) |
6 | | mbfsup.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | uzid 12458 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
9 | | mbfsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | 8, 9 | eleqtrrdi 2849 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
12 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
13 | 12, 3 | dmmptd 6528 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) = 𝑍) |
14 | 11, 13 | eleqtrrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ dom (𝑛 ∈ 𝑍 ↦ 𝐵)) |
15 | 14 | ne0d 4255 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
16 | | dm0rn0 5799 |
. . . . . 6
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) = ∅) |
17 | 16 | necon3bii 2993 |
. . . . 5
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
18 | 15, 17 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
19 | | mbfsup.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦) |
20 | 4 | ffnd 6551 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
21 | | breq1 5061 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
22 | 21 | ralrn 6912 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
23 | 20, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
24 | | nffvmpt1 6733 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
25 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
≤ |
26 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑦 |
27 | 24, 25, 26 | nfbr 5105 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 |
28 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 |
29 | | fveq2 6722 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
30 | 29 | breq1d 5068 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦)) |
31 | 27, 28, 30 | cbvralw 3354 |
. . . . . . . 8
⊢
(∀𝑚 ∈
𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦) |
32 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
33 | 12 | fvmpt2 6834 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℝ) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
34 | 32, 3, 33 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
35 | 34 | breq1d 5068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
36 | 35 | ralbidva 3117 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
37 | 31, 36 | syl5bb 286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
38 | 23, 37 | bitrd 282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
39 | 38 | rexbidv 3221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
40 | 19, 39 | mpbird 260 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) |
41 | 5, 18, 40 | suprcld 11800 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈
ℝ) |
42 | | mbfsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
43 | 41, 42 | fmptd 6936 |
. 2
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
44 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
45 | | ltso 10918 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
46 | 45 | supex 9084 |
. . . . . . . . . . . . 13
⊢ sup(ran
(𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V |
47 | 42 | fvmpt2 6834 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
48 | 44, 46, 47 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
49 | 48 | breq2d 5070 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))) |
50 | 5, 18, 40 | 3jca 1130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
51 | 50 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
52 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ ℝ) |
53 | | suprlub 11801 |
. . . . . . . . . . . 12
⊢ (((ran
(𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑡 ∈ ℝ) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
54 | 51, 52, 53 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
55 | 20 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
56 | | breq2 5062 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑡 < 𝑧 ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
57 | 56 | rexrn 6911 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
59 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑡 |
60 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
< |
61 | 59, 60, 24 | nfbr 5105 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
62 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) |
63 | 29 | breq2d 5070 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛))) |
64 | 61, 62, 63 | cbvrexw 3355 |
. . . . . . . . . . . . 13
⊢
(∃𝑚 ∈
𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
65 | 12 | fvmpt2i 6833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ( I ‘𝐵)) |
66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
67 | 66 | fvmpt2i 6833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
68 | 67 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
69 | 68 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( I ‘𝐵) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
70 | 65, 69 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
71 | 70 | breq2d 5070 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
72 | 71 | rexbidva 3220 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
73 | 72 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
74 | 64, 73 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
75 | 58, 74 | bitrd 282 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
76 | 49, 54, 75 | 3bitrd 308 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
77 | 76 | ralrimiva 3105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
78 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
79 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑡 |
80 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
< |
81 | | nfmpt1 5158 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
82 | 42, 81 | nfcxfr 2902 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐺 |
83 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑧 |
84 | 82, 83 | nffv 6732 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝐺‘𝑧) |
85 | 79, 80, 84 | nfbr 5105 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑡 < (𝐺‘𝑧) |
86 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑍 |
87 | | nffvmpt1 6733 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
88 | 79, 80, 87 | nfbr 5105 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
89 | 86, 88 | nfrex 3233 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
90 | 85, 89 | nfbi 1911 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
91 | | fveq2 6722 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
92 | 91 | breq2d 5070 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < (𝐺‘𝑧))) |
93 | | fveq2 6722 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
94 | 93 | breq2d 5070 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
95 | 94 | rexbidv 3221 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
96 | 92, 95 | bibi12d 349 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
97 | 78, 90, 96 | cbvralw 3354 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
98 | 77, 97 | sylib 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
99 | 98 | r19.21bi 3130 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
100 | 43 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺:𝐴⟶ℝ) |
101 | 100 | ffvelrnda 6909 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) |
102 | | rexr 10884 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℝ*) |
103 | 102 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑡 ∈ ℝ*) |
104 | | elioopnf 13036 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ*
→ ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
105 | 103, 104 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
106 | 101, 105 | mpbirand 707 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < (𝐺‘𝑧))) |
107 | 103 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑡 ∈ ℝ*) |
108 | | elioopnf 13036 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ*
→ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
110 | 2 | fmpttd 6937 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) |
111 | 110 | ffvelrnda 6909 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ) |
112 | 111 | biantrurd 536 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
113 | 112 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
114 | 113 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
115 | 109, 114 | bitr4d 285 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
116 | 115 | rexbidva 3220 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
117 | 99, 106, 116 | 3bitr4d 314 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
118 | 117 | pm5.32da 582 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
119 | 43 | ffnd 6551 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
120 | 119 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺 Fn 𝐴) |
121 | | elpreima 6883 |
. . . . . 6
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
122 | 120, 121 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
123 | | eliun 4913 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
124 | 110 | ffnd 6551 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
125 | | elpreima 6883 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
126 | 124, 125 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
127 | 126 | rexbidva 3220 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
128 | 127 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
129 | | r19.42v 3268 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
130 | 128, 129 | bitrdi 290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
131 | 123, 130 | syl5bb 286 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
132 | 118, 122,
131 | 3bitr4d 314 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ 𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)))) |
133 | 132 | eqrdv 2735 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) = ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
134 | | zex 12190 |
. . . . . . 7
⊢ ℤ
∈ V |
135 | | uzssz 12464 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
136 | | ssdomg 8679 |
. . . . . . 7
⊢ (ℤ
∈ V → ((ℤ≥‘𝑀) ⊆ ℤ →
(ℤ≥‘𝑀) ≼ ℤ)) |
137 | 134, 135,
136 | mp2 9 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ≼ ℤ |
138 | 9, 137 | eqbrtri 5079 |
. . . . 5
⊢ 𝑍 ≼
ℤ |
139 | | znnen 15778 |
. . . . 5
⊢ ℤ
≈ ℕ |
140 | | domentr 8692 |
. . . . 5
⊢ ((𝑍 ≼ ℤ ∧ ℤ
≈ ℕ) → 𝑍
≼ ℕ) |
141 | 138, 139,
140 | mp2an 692 |
. . . 4
⊢ 𝑍 ≼
ℕ |
142 | | mbfsup.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
143 | | mbfima 24532 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
144 | 142, 110,
143 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
145 | 144 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
146 | 145 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
147 | | iunmbl2 24459 |
. . . 4
⊢ ((𝑍 ≼ ℕ ∧
∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
148 | 141, 146,
147 | sylancr 590 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
149 | 133, 148 | eqeltrd 2838 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) ∈ dom
vol) |
150 | 43, 149 | ismbf3d 24556 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |