Proof of Theorem ovolval4lem1
Step | Hyp | Ref
| Expression |
1 | | ioof 13179 |
. . . . . . . 8
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (,):(ℝ*
× ℝ*)⟶𝒫 ℝ) |
3 | | ovolval4lem1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
4 | | fco 6624 |
. . . . . . 7
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
5 | 2, 3, 4 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
6 | 5 | ffnd 6601 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
7 | | fniunfv 7120 |
. . . . 5
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
9 | 8 | eqcomd 2744 |
. . 3
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛)) |
10 | | ovolval4lem1.a |
. . . . . . . . 9
⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} |
11 | | ssrab2 4013 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣
(1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ |
12 | 10, 11 | eqsstri 3955 |
. . . . . . . 8
⊢ 𝐴 ⊆
ℕ |
13 | | undif 4415 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ) |
14 | 12, 13 | mpbi 229 |
. . . . . . 7
⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ |
15 | 14 | eqcomi 2747 |
. . . . . 6
⊢ ℕ =
(𝐴 ∪ (ℕ ∖
𝐴)) |
16 | 15 | iuneq1i 42635 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) |
17 | | iunxun 5023 |
. . . . 5
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
18 | 16, 17 | eqtri 2766 |
. . . 4
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
20 | 3 | ffvelrnda 6961 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* ×
ℝ*)) |
21 | | xp1st 7863 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ*) |
23 | | xp2nd 7864 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
25 | 24, 22 | ifcld 4505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))) ∈
ℝ*) |
26 | 22, 25 | opelxpd 5627 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
(ℝ* × ℝ*)) |
27 | | ovolval4lem1.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉) |
28 | 26, 27 | fmptd 6988 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
29 | | fco 6624 |
. . . . . . . 8
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
30 | 2, 28, 29 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
31 | 30 | ffnd 6601 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
32 | | fniunfv 7120 |
. . . . . 6
⊢ (((,)
∘ 𝐺) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
34 | 33 | eqcomd 2744 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐺)‘𝑛)) |
35 | 15 | iuneq1i 42635 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) |
36 | | iunxun 5023 |
. . . . . 6
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
37 | 35, 36 | eqtri 2766 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛))) |
39 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
40 | 12 | sseli 3917 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ) |
41 | 40 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ) |
42 | | fvco3 6867 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
43 | 39, 41, 42 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
44 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
45 | | fvco3 6867 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
46 | 44, 41, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
47 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑) |
48 | | 1st2nd2 7870 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
49 | 20, 48 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
50 | 47, 41, 49 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
51 | 27 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉)) |
52 | 26 | elexd 3452 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
V) |
53 | 51, 52 | fvmpt2d 6888 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
54 | 47, 41, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
55 | 10 | eleq2i 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
56 | 55 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
57 | | rabid 3310 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
58 | 56, 57 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
59 | 58 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
61 | 60 | iftrued 4467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛))) |
62 | 61 | opeq2d 4811 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
63 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
64 | 54, 62, 63 | 3eqtrd 2782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
65 | 50, 64 | eqtr4d 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
66 | 65 | fveq2d 6778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛))) |
67 | 46, 66 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
68 | 43, 67 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
69 | 68 | iuneq2dv 4948 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛)) |
70 | 28 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
71 | | eldifi 4061 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ) |
72 | 71 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ) |
73 | 70, 72, 42 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
74 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑) |
75 | 74, 72, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
76 | 71 | anim1i 615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
77 | 76, 57 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
78 | 77, 55 | sylibr 233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
79 | 78 | adantll 711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
80 | | eldifn 4062 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴) |
81 | 80 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
82 | 79, 81 | pm2.65da 814 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
83 | 82 | iffalsed 4470 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛))) |
84 | 83 | opeq2d 4811 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 =
〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
85 | 75, 84 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
86 | 85 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉)) |
87 | | iooid 13107 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅ |
88 | 87 | eqcomi 2747 |
. . . . . . . . . . 11
⊢ ∅ =
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) |
89 | | df-ov 7278 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) |
90 | 88, 89 | eqtr2i 2767 |
. . . . . . . . . 10
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) = ∅ |
91 | 90 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) =
∅) |
92 | 73, 86, 91 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅) |
93 | 92 | iuneq2dv 4948 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
94 | | iun0 4991 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅ |
95 | 94 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅) |
96 | 93, 95 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅) |
97 | 74, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
98 | 97, 72, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
99 | 74, 72, 49 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
100 | 99 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
101 | | df-ov 7278 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
102 | 101 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
103 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
104 | 72, 22 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
105 | 104 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
106 | 72, 24 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
108 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛))) |
109 | 105, 107 | xrltnled 42902 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))) |
110 | 108, 109 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛))) |
111 | 105, 107,
110 | xrltled 12884 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
112 | 103, 111,
78 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
113 | 80 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
114 | 112, 113 | condan 815 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) |
115 | | ioo0 13104 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ*) →
(((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
116 | 104, 106,
115 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
117 | 114, 116 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅) |
118 | 102, 117 | eqtr3d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) =
∅) |
119 | 98, 100, 118 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅) |
120 | 119 | iuneq2dv 4948 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
121 | 120, 95 | eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅) |
122 | 96, 121 | eqtr4d 2781 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) |
123 | 69, 122 | uneq12d 4098 |
. . . 4
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
124 | 34, 38, 123 | 3eqtrrd 2783 |
. . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,)
∘ 𝐺)) |
125 | 9, 19, 124 | 3eqtrd 2782 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺)) |
126 | | volf 24693 |
. . . . . 6
⊢ vol:dom
vol⟶(0[,]+∞) |
127 | 126 | a1i 11 |
. . . . 5
⊢ (𝜑 → vol:dom
vol⟶(0[,]+∞)) |
128 | 3 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
129 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
130 | 128, 129,
45 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
131 | 49 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
132 | 101 | eqcomi 2747 |
. . . . . . . . . . 11
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) |
133 | 132 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
134 | 130, 131,
133 | 3eqtrd 2782 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
135 | | ioombl 24729 |
. . . . . . . . . 10
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol |
136 | 135 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ∈ dom
vol) |
137 | 134, 136 | eqeltrd 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
138 | 137 | ralrimiva 3103 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
139 | 6, 138 | jca 512 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐹)‘𝑛) ∈ dom vol)) |
140 | | ffnfv 6992 |
. . . . . 6
⊢ (((,)
∘ 𝐹):ℕ⟶dom vol ↔ (((,)
∘ 𝐹) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐹)‘𝑛) ∈ dom vol)) |
141 | 139, 140 | sylibr 233 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom
vol) |
142 | | fco 6624 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞)) |
143 | 127, 141,
142 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)):ℕ⟶(0[,]+∞)) |
144 | 143 | ffnd 6601 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) Fn
ℕ) |
145 | 68 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
146 | 137 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
147 | 145, 146 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
148 | | simpll 764 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑) |
149 | | eldif 3897 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴)) |
150 | 149 | bicomi 223 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴)) |
151 | 150 | biimpi 215 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
152 | 151 | adantll 711 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
153 | 117, 135 | eqeltrrdi 2848 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom
vol) |
154 | 92, 153 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
155 | 148, 152,
154 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
156 | 147, 155 | pm2.61dan 810 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
157 | 156 | ralrimiva 3103 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
158 | 31, 157 | jca 512 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐺)‘𝑛) ∈ dom vol)) |
159 | | ffnfv 6992 |
. . . . . 6
⊢ (((,)
∘ 𝐺):ℕ⟶dom vol ↔ (((,)
∘ 𝐺) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐺)‘𝑛) ∈ dom vol)) |
160 | 158, 159 | sylibr 233 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom
vol) |
161 | | fco 6624 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞)) |
162 | 127, 160,
161 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)):ℕ⟶(0[,]+∞)) |
163 | 162 | ffnd 6601 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)) Fn
ℕ) |
164 | 145 | eqcomd 2744 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
165 | 119, 92 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
166 | 148, 152,
165 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
167 | 164, 166 | pm2.61dan 810 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
168 | 167 | fveq2d 6778 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,)
∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
169 | | fnfun 6533 |
. . . . . . 7
⊢ (((,)
∘ 𝐹) Fn ℕ
→ Fun ((,) ∘ 𝐹)) |
170 | 6, 169 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐹)) |
171 | 170 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐹)) |
172 | 5 | fdmd 6611 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ) |
173 | 172 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐹)) |
174 | 173 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐹)) |
175 | 129, 174 | eleqtrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹)) |
176 | | fvco 6866 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
177 | 171, 175,
176 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
178 | | fnfun 6533 |
. . . . . . 7
⊢ (((,)
∘ 𝐺) Fn ℕ
→ Fun ((,) ∘ 𝐺)) |
179 | 31, 178 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐺)) |
180 | 179 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐺)) |
181 | 30 | fdmd 6611 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ) |
182 | 181 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐺)) |
183 | 182 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐺)) |
184 | 129, 183 | eleqtrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺)) |
185 | | fvco 6866 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
186 | 180, 184,
185 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
187 | 168, 177,
186 | 3eqtr4d 2788 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘
𝐺))‘𝑛)) |
188 | 144, 163,
187 | eqfnfvd 6912 |
. 2
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) = (vol ∘ ((,)
∘ 𝐺))) |
189 | 125, 188 | jca 512 |
1
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺) ∧ (vol
∘ ((,) ∘ 𝐹)) =
(vol ∘ ((,) ∘ 𝐺)))) |