Step | Hyp | Ref
| Expression |
1 | | mbfsup.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ) |
2 | 1 | anassrs 678 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
3 | 2 | an32s 842 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
5 | 3, 4 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ) |
6 | | frn 5966 |
. . . . 5
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ) |
8 | | mbfsup.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | | uzid 11578 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
11 | | mbfsup.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
12 | 10, 11 | syl6eleqr 2699 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍) |
14 | 4, 3 | dmmptd 5937 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) = 𝑍) |
15 | 13, 14 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ dom (𝑛 ∈ 𝑍 ↦ 𝐵)) |
16 | | ne0i 3880 |
. . . . . 6
⊢ (𝑀 ∈ dom (𝑛 ∈ 𝑍 ↦ 𝐵) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
18 | | dm0rn0 5263 |
. . . . . 6
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) = ∅) |
19 | 18 | necon3bii 2834 |
. . . . 5
⊢ (dom
(𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
20 | 17, 19 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅) |
21 | | mbfsup.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦) |
22 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
23 | 5, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
24 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
25 | 24 | ralrn 6270 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
26 | 23, 25 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦)) |
27 | | nffvmpt1 6111 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
28 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
≤ |
29 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑦 |
30 | 27, 28, 29 | nfbr 4629 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 |
31 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑚((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 |
32 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
33 | 32 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦)) |
34 | 30, 31, 33 | cbvral 3143 |
. . . . . . . 8
⊢
(∀𝑚 ∈
𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦) |
35 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
36 | 4 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℝ) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
37 | 35, 3, 36 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵) |
38 | 37 | breq1d 4593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
39 | 38 | ralbidva 2968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
40 | 34, 39 | syl5bb 271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
41 | 26, 40 | bitrd 267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
42 | 41 | rexbidv 3034 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)) |
43 | 21, 42 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) |
44 | | suprcl 10862 |
. . . 4
⊢ ((ran
(𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) → sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈
ℝ) |
45 | 7, 20, 43, 44 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈
ℝ) |
46 | | mbfsup.2 |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
47 | 45, 46 | fmptd 6292 |
. 2
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
48 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
49 | | ltso 9997 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
50 | 49 | supex 8252 |
. . . . . . . . . . . . 13
⊢ sup(ran
(𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V |
51 | 46 | fvmpt2 6200 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
52 | 48, 50, 51 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
53 | 52 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))) |
54 | 7, 20, 43 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
55 | 54 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)) |
56 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ ℝ) |
57 | | suprlub 10864 |
. . . . . . . . . . . 12
⊢ (((ran
(𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑡 ∈ ℝ) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
58 | 55, 56, 57 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧)) |
59 | 23 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍) |
60 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑡 < 𝑧 ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
61 | 60 | rexrn 6269 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚))) |
63 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑡 |
64 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
< |
65 | 63, 64, 27 | nfbr 4629 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) |
66 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) |
67 | 32 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛))) |
68 | 65, 66, 67 | cbvrex 3144 |
. . . . . . . . . . . . 13
⊢
(∃𝑚 ∈
𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)) |
69 | 4 | fvmpt2i 6199 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ( I ‘𝐵)) |
70 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
71 | 70 | fvmpt2i 6199 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵)) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( I ‘𝐵) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
74 | 69, 73 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
75 | 74 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
76 | 75 | rexbidva 3031 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
77 | 76 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
78 | 68, 77 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
79 | 62, 78 | bitrd 267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
80 | 53, 58, 79 | 3bitrd 293 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
81 | 80 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
82 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
83 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑡 |
84 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
< |
85 | | nfmpt1 4675 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )) |
86 | 46, 85 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐺 |
87 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑧 |
88 | 86, 87 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝐺‘𝑧) |
89 | 83, 84, 88 | nfbr 4629 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑡 < (𝐺‘𝑧) |
90 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑍 |
91 | | nffvmpt1 6111 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
92 | 83, 84, 91 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
93 | 90, 92 | nfrex 2990 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) |
94 | 89, 93 | nfbi 1821 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
95 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
96 | 95 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < (𝐺‘𝑧))) |
97 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
98 | 97 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
99 | 98 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
100 | 96, 99 | bibi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
101 | 82, 94, 100 | cbvral 3143 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
102 | 81, 101 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
103 | 102 | r19.21bi 2916 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
104 | | rexr 9964 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℝ*) |
105 | 104 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑡 ∈ ℝ*) |
106 | | elioopnf 12138 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ*
→ ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
107 | 105, 106 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
108 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺:𝐴⟶ℝ) |
109 | 108 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ) |
110 | 109 | biantrurd 528 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑡 < (𝐺‘𝑧) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧)))) |
111 | 107, 110 | bitr4d 270 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < (𝐺‘𝑧))) |
112 | 105 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑡 ∈ ℝ*) |
113 | | elioopnf 12138 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ*
→ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
115 | 2, 70 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) |
116 | 115 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ) |
117 | 116 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
118 | 117 | an32s 842 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
119 | 118 | adantllr 751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))) |
120 | 114, 119 | bitr4d 270 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
121 | 120 | rexbidva 3031 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))) |
122 | 103, 111,
121 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
123 | 122 | pm5.32da 671 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
124 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:𝐴⟶ℝ → 𝐺 Fn 𝐴) |
125 | 47, 124 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
126 | 125 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺 Fn 𝐴) |
127 | | elpreima 6245 |
. . . . . 6
⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
128 | 126, 127 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)))) |
129 | | eliun 4460 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
130 | | ffn 5958 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
131 | 115, 130 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
132 | | elpreima 6245 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
134 | 133 | rexbidva 3031 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
135 | 134 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
136 | | r19.42v 3073 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))) |
137 | 135, 136 | syl6bb 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
138 | 129, 137 | syl5bb 271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))) |
139 | 123, 128,
138 | 3bitr4d 299 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (◡𝐺 “ (𝑡(,)+∞)) ↔ 𝑧 ∈ ∪
𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)))) |
140 | 139 | eqrdv 2608 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) = ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))) |
141 | | zex 11263 |
. . . . . . 7
⊢ ℤ
∈ V |
142 | | uzssz 11583 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
143 | | ssdomg 7887 |
. . . . . . 7
⊢ (ℤ
∈ V → ((ℤ≥‘𝑀) ⊆ ℤ →
(ℤ≥‘𝑀) ≼ ℤ)) |
144 | 141, 142,
143 | mp2 9 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ≼ ℤ |
145 | 11, 144 | eqbrtri 4604 |
. . . . 5
⊢ 𝑍 ≼
ℤ |
146 | | znnen 14780 |
. . . . 5
⊢ ℤ
≈ ℕ |
147 | | domentr 7901 |
. . . . 5
⊢ ((𝑍 ≼ ℤ ∧ ℤ
≈ ℕ) → 𝑍
≼ ℕ) |
148 | 145, 146,
147 | mp2an 704 |
. . . 4
⊢ 𝑍 ≼
ℕ |
149 | | mbfsup.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
150 | | mbfima 23205 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
151 | 149, 115,
150 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
152 | 151 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
153 | 152 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
154 | | iunmbl2 23132 |
. . . 4
⊢ ((𝑍 ≼ ℕ ∧
∀𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
155 | 148, 153,
154 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∪ 𝑛 ∈ 𝑍 (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom
vol) |
156 | 140, 155 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (◡𝐺 “ (𝑡(,)+∞)) ∈ dom
vol) |
157 | 47, 156 | ismbf3d 23227 |
1
⊢ (𝜑 → 𝐺 ∈ MblFn) |