Proof of Theorem ovolval4lem1
Step | Hyp | Ref
| Expression |
1 | | ioof 12142 |
. . . . . . . 8
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (,):(ℝ*
× ℝ*)⟶𝒫 ℝ) |
3 | | ovolval4lem1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
4 | | fco 5971 |
. . . . . . 7
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
5 | 2, 3, 4 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
6 | | ffn 5958 |
. . . . . 6
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
8 | | fniunfv 6409 |
. . . . 5
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
10 | 9 | eqcomd 2616 |
. . 3
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛)) |
11 | | ovolval4lem1.a |
. . . . . . . . 9
⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} |
12 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣
(1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ |
13 | 11, 12 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝐴 ⊆
ℕ |
14 | | undif 4001 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ) |
15 | 13, 14 | mpbi 219 |
. . . . . . 7
⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ |
16 | 15 | eqcomi 2619 |
. . . . . 6
⊢ ℕ =
(𝐴 ∪ (ℕ ∖
𝐴)) |
17 | 16 | iuneq1i 38286 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) |
18 | | iunxun 4541 |
. . . . 5
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
19 | 17, 18 | eqtri 2632 |
. . . 4
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
20 | 19 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
21 | 3 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* ×
ℝ*)) |
22 | | xp1st 7089 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ*) |
24 | | xp2nd 7090 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
25 | 21, 24 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
26 | 25, 23 | ifcld 4081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))) ∈
ℝ*) |
27 | 23, 26 | opelxpd 5073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
(ℝ* × ℝ*)) |
28 | | ovolval4lem1.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉) |
29 | 27, 28 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
30 | | fco 5971 |
. . . . . . . 8
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
31 | 2, 29, 30 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
32 | | ffn 5958 |
. . . . . . 7
⊢ (((,)
∘ 𝐺):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐺) Fn
ℕ) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
34 | | fniunfv 6409 |
. . . . . 6
⊢ (((,)
∘ 𝐺) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
36 | 35 | eqcomd 2616 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐺)‘𝑛)) |
37 | 16 | iuneq1i 38286 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) |
38 | | iunxun 4541 |
. . . . . 6
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
39 | 37, 38 | eqtri 2632 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
40 | 39 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛))) |
41 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
42 | 13 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ) |
44 | | fvco3 6185 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
45 | 41, 43, 44 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
46 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
47 | | fvco3 6185 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
48 | 46, 43, 47 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
49 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑) |
50 | | 1st2nd2 7096 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
51 | 21, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
52 | 49, 43, 51 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
53 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉)) |
54 | 27 | elexd 3187 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
V) |
55 | 53, 54 | fvmpt2d 6202 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
56 | 49, 43, 55 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
57 | 11 | eleq2i 2680 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
58 | 57 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
59 | | rabid 3095 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
60 | 58, 59 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
61 | 60 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
63 | 62 | iftrued 4044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛))) |
64 | 63 | opeq2d 4347 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
65 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
66 | 56, 64, 65 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
67 | 52, 66 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
68 | 67 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛))) |
69 | 48, 68 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
70 | 45, 69 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
71 | 70 | iuneq2dv 4478 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛)) |
72 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
73 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ) |
74 | 73 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ) |
75 | 72, 74, 44 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
76 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑) |
77 | 76, 74, 55 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
78 | 73 | anim1i 590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
79 | 78, 59 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
80 | 79, 57 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
81 | 80 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
82 | | eldifn 3695 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴) |
83 | 82 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
84 | 81, 83 | pm2.65da 598 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
85 | 84 | iffalsed 4047 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛))) |
86 | 85 | opeq2d 4347 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 =
〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
87 | 77, 86 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
88 | 87 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉)) |
89 | | iooid 12074 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅ |
90 | 89 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ ∅ =
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) |
91 | | df-ov 6552 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) |
92 | 90, 91 | eqtr2i 2633 |
. . . . . . . . . 10
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) = ∅ |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) =
∅) |
94 | 75, 88, 93 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅) |
95 | 94 | iuneq2dv 4478 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
96 | | iun0 4512 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅ |
97 | 96 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅) |
98 | 95, 97 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅) |
99 | 76, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
100 | 99, 74, 47 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
101 | 76, 74, 51 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
102 | 101 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
103 | | df-ov 6552 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
105 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
106 | 74, 23 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
108 | 74, 25 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
110 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛))) |
111 | 107, 109 | xrltnled 38520 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))) |
112 | 110, 111 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛))) |
113 | 107, 109,
112 | xrltled 38427 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
114 | 105, 113,
80 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
115 | 82 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
116 | 114, 115 | condan 831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) |
117 | | ioo0 12071 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ*) →
(((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
118 | 106, 108,
117 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
119 | 116, 118 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅) |
120 | 104, 119 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) =
∅) |
121 | 100, 102,
120 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅) |
122 | 121 | iuneq2dv 4478 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
123 | 122, 97 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅) |
124 | 98, 123 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) |
125 | 71, 124 | uneq12d 3730 |
. . . 4
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
126 | 36, 40, 125 | 3eqtrrd 2649 |
. . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,)
∘ 𝐺)) |
127 | 10, 20, 126 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺)) |
128 | | volf 23104 |
. . . . . 6
⊢ vol:dom
vol⟶(0[,]+∞) |
129 | 128 | a1i 11 |
. . . . 5
⊢ (𝜑 → vol:dom
vol⟶(0[,]+∞)) |
130 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
131 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
132 | 130, 131,
47 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
133 | 51 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
134 | 103 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) |
135 | 134 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
136 | 132, 133,
135 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
137 | | ioombl 23140 |
. . . . . . . . . 10
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol |
138 | 137 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ∈ dom
vol) |
139 | 136, 138 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
140 | 139 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
141 | 7, 140 | jca 553 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐹)‘𝑛) ∈ dom vol)) |
142 | | ffnfv 6295 |
. . . . . 6
⊢ (((,)
∘ 𝐹):ℕ⟶dom vol ↔ (((,)
∘ 𝐹) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐹)‘𝑛) ∈ dom vol)) |
143 | 141, 142 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom
vol) |
144 | | fco 5971 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞)) |
145 | 129, 143,
144 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)):ℕ⟶(0[,]+∞)) |
146 | | ffn 5958 |
. . . 4
⊢ ((vol
∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞) → (vol
∘ ((,) ∘ 𝐹)) Fn
ℕ) |
147 | 145, 146 | syl 17 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) Fn
ℕ) |
148 | 70 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
149 | 139 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
150 | 148, 149 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
151 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑) |
152 | | eldif 3550 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴)) |
153 | 152 | bicomi 213 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴)) |
154 | 153 | biimpi 205 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
155 | 154 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
156 | 119, 137 | syl6eqelr 2697 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom
vol) |
157 | 94, 156 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
158 | 151, 155,
157 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
159 | 150, 158 | pm2.61dan 828 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
160 | 159 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
161 | 33, 160 | jca 553 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐺)‘𝑛) ∈ dom vol)) |
162 | | ffnfv 6295 |
. . . . . 6
⊢ (((,)
∘ 𝐺):ℕ⟶dom vol ↔ (((,)
∘ 𝐺) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐺)‘𝑛) ∈ dom vol)) |
163 | 161, 162 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom
vol) |
164 | | fco 5971 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞)) |
165 | 129, 163,
164 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)):ℕ⟶(0[,]+∞)) |
166 | | ffn 5958 |
. . . 4
⊢ ((vol
∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞) → (vol
∘ ((,) ∘ 𝐺)) Fn
ℕ) |
167 | 165, 166 | syl 17 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)) Fn
ℕ) |
168 | 148 | eqcomd 2616 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
169 | 121, 94 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
170 | 151, 155,
169 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
171 | 168, 170 | pm2.61dan 828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
172 | 171 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,)
∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
173 | | fnfun 5902 |
. . . . . . 7
⊢ (((,)
∘ 𝐹) Fn ℕ
→ Fun ((,) ∘ 𝐹)) |
174 | 7, 173 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐹)) |
175 | 174 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐹)) |
176 | | fdm 5964 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐹):ℕ⟶dom vol → dom ((,)
∘ 𝐹) =
ℕ) |
177 | 143, 176 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ) |
178 | 177 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐹)) |
179 | 178 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐹)) |
180 | 131, 179 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹)) |
181 | | fvco 6184 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
182 | 175, 180,
181 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
183 | | fnfun 5902 |
. . . . . . 7
⊢ (((,)
∘ 𝐺) Fn ℕ
→ Fun ((,) ∘ 𝐺)) |
184 | 33, 183 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐺)) |
185 | 184 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐺)) |
186 | | fdm 5964 |
. . . . . . . . 9
⊢ (((,)
∘ 𝐺):ℕ⟶dom vol → dom ((,)
∘ 𝐺) =
ℕ) |
187 | 163, 186 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ) |
188 | 187 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐺)) |
189 | 188 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐺)) |
190 | 131, 189 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺)) |
191 | | fvco 6184 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
192 | 185, 190,
191 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
193 | 172, 182,
192 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘
𝐺))‘𝑛)) |
194 | 147, 167,
193 | eqfnfvd 6222 |
. 2
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) = (vol ∘ ((,)
∘ 𝐺))) |
195 | 127, 194 | jca 553 |
1
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺) ∧ (vol
∘ ((,) ∘ 𝐹)) =
(vol ∘ ((,) ∘ 𝐺)))) |