Proof of Theorem ovolval4lem1
| Step | Hyp | Ref
| Expression |
| 1 | | ioof 13487 |
. . . . . . . 8
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 2 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (,):(ℝ*
× ℝ*)⟶𝒫 ℝ) |
| 3 | | ovolval4lem1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 4 | | fco 6760 |
. . . . . . 7
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 6 | 5 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ) |
| 7 | | fniunfv 7267 |
. . . . 5
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
| 8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
| 9 | 8 | eqcomd 2743 |
. . 3
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛)) |
| 10 | | ovolval4lem1.a |
. . . . . . . . 9
⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} |
| 11 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ ∣
(1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ |
| 12 | 10, 11 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝐴 ⊆
ℕ |
| 13 | | undif 4482 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ) |
| 14 | 12, 13 | mpbi 230 |
. . . . . . 7
⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ |
| 15 | 14 | eqcomi 2746 |
. . . . . 6
⊢ ℕ =
(𝐴 ∪ (ℕ ∖
𝐴)) |
| 16 | 15 | iuneq1i 45090 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) |
| 17 | | iunxun 5094 |
. . . . 5
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
| 18 | 16, 17 | eqtri 2765 |
. . . 4
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) |
| 19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
| 20 | 3 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* ×
ℝ*)) |
| 21 | | xp1st 8046 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ*) |
| 23 | | xp2nd 8047 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ (ℝ* ×
ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 24 | 20, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
| 25 | 24, 22 | ifcld 4572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))) ∈
ℝ*) |
| 26 | 22, 25 | opelxpd 5724 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
(ℝ* × ℝ*)) |
| 27 | | ovolval4lem1.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉) |
| 28 | 26, 27 | fmptd 7134 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 29 | | fco 6760 |
. . . . . . . 8
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 30 | 2, 28, 29 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 31 | 30 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ) |
| 32 | | fniunfv 7267 |
. . . . . 6
⊢ (((,)
∘ 𝐺) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,)
∘ 𝐺)) |
| 34 | 33 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪
𝑛 ∈ ℕ (((,)
∘ 𝐺)‘𝑛)) |
| 35 | 15 | iuneq1i 45090 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) |
| 36 | | iunxun 5094 |
. . . . . 6
⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
| 37 | 35, 36 | eqtri 2765 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) |
| 38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛))) |
| 39 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 40 | 12 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ) |
| 41 | 40 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ) |
| 42 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
| 43 | 39, 41, 42 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
| 44 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 45 | | fvco3 7008 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(ℝ* ×
ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 46 | 44, 41, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 47 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑) |
| 48 | | 1st2nd2 8053 |
. . . . . . . . . . . 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 3504 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 ∈
V) |
| 53 | 51, 52 | fvmpt2d 7029 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
| 54 | 47, 41, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) |
| 55 | 10 | eleq2i 2833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
| 56 | 55 | biimpi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
| 57 | | rabid 3458 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
| 58 | 56, 57 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
| 59 | 58 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
| 61 | 60 | iftrued 4533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛))) |
| 62 | 61 | opeq2d 4880 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
| 63 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉 = 〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
| 64 | 54, 62, 63 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
| 65 | 50, 64 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
| 66 | 65 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛))) |
| 67 | 46, 66 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
| 68 | 43, 67 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
| 69 | 68 | iuneq2dv 5016 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛)) |
| 70 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 71 | | eldifi 4131 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ) |
| 72 | 71 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ) |
| 73 | 70, 72, 42 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛))) |
| 74 | | simpl 482 |
. . . . . . . . . . . 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 234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))}) |
| 78 | 77, 55 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
| 79 | 78 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
| 80 | | eldifn 4132 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴) |
| 81 | 80 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
| 82 | 79, 81 | pm2.65da 817 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
| 83 | 82 | iffalsed 4536 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛))) |
| 84 | 83 | opeq2d 4880 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 〈(1st
‘(𝐹‘𝑛)), if((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛)))〉 =
〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
| 85 | 75, 84 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉)) |
| 87 | | iooid 13415 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅ |
| 88 | 87 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ ∅ =
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) |
| 89 | | df-ov 7434 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) |
| 90 | 88, 89 | eqtr2i 2766 |
. . . . . . . . . 10
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))〉) = ∅ |
| 91 | 90 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (1st
‘(𝐹‘𝑛))〉) =
∅) |
| 92 | 73, 86, 91 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅) |
| 93 | 92 | iuneq2dv 5016 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
| 94 | | iun0 5062 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅ |
| 95 | 94 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅) |
| 96 | 93, 95 | eqtrd 2777 |
. . . . . 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 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
| 101 | | df-ov 7434 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
| 102 | 101 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
| 103 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
| 104 | 72, 22 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 105 | 104 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 106 | 72, 24 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 107 | 106 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈
ℝ*) |
| 108 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛))) |
| 109 | 105, 107 | xrltnled 45374 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))) |
| 110 | 108, 109 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛))) |
| 111 | 105, 107,
110 | xrltled 13192 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) |
| 112 | 103, 111,
78 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴) |
| 113 | 80 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴) |
| 114 | 112, 113 | condan 818 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) |
| 115 | | ioo0 13412 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ*) →
(((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
| 116 | 104, 106,
115 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd
‘(𝐹‘𝑛)) ≤ (1st
‘(𝐹‘𝑛)))) |
| 117 | 114, 116 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅) |
| 118 | 102, 117 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) =
∅) |
| 119 | 98, 100, 118 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅) |
| 120 | 119 | iuneq2dv 5016 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅) |
| 121 | 120, 95 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅) |
| 122 | 96, 121 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) |
| 123 | 69, 122 | uneq12d 4169 |
. . . 4
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪
𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛))) |
| 124 | 34, 38, 123 | 3eqtrrd 2782 |
. . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪
𝑛 ∈ (ℕ ∖
𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,)
∘ 𝐺)) |
| 125 | 9, 19, 124 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺)) |
| 126 | | volf 25564 |
. . . . . 6
⊢ vol:dom
vol⟶(0[,]+∞) |
| 127 | 126 | a1i 11 |
. . . . 5
⊢ (𝜑 → vol:dom
vol⟶(0[,]+∞)) |
| 128 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 129 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 130 | 128, 129,
45 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 131 | 49 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
| 132 | 101 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) |
| 133 | 132 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((,)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 134 | 130, 131,
133 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 135 | | ioombl 25600 |
. . . . . . . . . 10
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol |
| 136 | 135 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ∈ dom
vol) |
| 137 | 134, 136 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 138 | 137 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 139 | 6, 138 | jca 511 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐹)‘𝑛) ∈ dom vol)) |
| 140 | | ffnfv 7139 |
. . . . . 6
⊢ (((,)
∘ 𝐹):ℕ⟶dom vol ↔ (((,)
∘ 𝐹) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐹)‘𝑛) ∈ dom vol)) |
| 141 | 139, 140 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom
vol) |
| 142 | | fco 6760 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞)) |
| 143 | 127, 141,
142 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)):ℕ⟶(0[,]+∞)) |
| 144 | 143 | ffnd 6737 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) Fn
ℕ) |
| 145 | 68 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛)) |
| 146 | 137 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol) |
| 147 | 145, 146 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
| 148 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑) |
| 149 | | eldif 3961 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴)) |
| 150 | 149 | bicomi 224 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴)) |
| 151 | 150 | biimpi 216 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ ¬
𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
| 152 | 151 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴)) |
| 153 | 117, 135 | eqeltrrdi 2850 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom
vol) |
| 154 | 92, 153 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
| 155 | 148, 152,
154 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
| 156 | 147, 155 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
| 157 | 156 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol) |
| 158 | 31, 157 | jca 511 |
. . . . . 6
⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘
𝐺)‘𝑛) ∈ dom vol)) |
| 159 | | ffnfv 7139 |
. . . . . 6
⊢ (((,)
∘ 𝐺):ℕ⟶dom vol ↔ (((,)
∘ 𝐺) Fn ℕ ∧
∀𝑛 ∈ ℕ
(((,) ∘ 𝐺)‘𝑛) ∈ dom vol)) |
| 160 | 158, 159 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom
vol) |
| 161 | | fco 6760 |
. . . . 5
⊢ ((vol:dom
vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol
∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞)) |
| 162 | 127, 160,
161 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)):ℕ⟶(0[,]+∞)) |
| 163 | 162 | ffnd 6737 |
. . 3
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐺)) Fn
ℕ) |
| 164 | 145 | eqcomd 2743 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
| 165 | 119, 92 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
| 166 | 148, 152,
165 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
| 167 | 164, 166 | pm2.61dan 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛)) |
| 168 | 167 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,)
∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
| 169 | | fnfun 6668 |
. . . . . . 7
⊢ (((,)
∘ 𝐹) Fn ℕ
→ Fun ((,) ∘ 𝐹)) |
| 170 | 6, 169 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐹)) |
| 171 | 170 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐹)) |
| 172 | 5 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ) |
| 173 | 172 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐹)) |
| 174 | 173 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐹)) |
| 175 | 129, 174 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹)) |
| 176 | | fvco 7007 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
| 177 | 171, 175,
176 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = (vol‘(((,) ∘
𝐹)‘𝑛))) |
| 178 | | fnfun 6668 |
. . . . . . 7
⊢ (((,)
∘ 𝐺) Fn ℕ
→ Fun ((,) ∘ 𝐺)) |
| 179 | 31, 178 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun ((,) ∘ 𝐺)) |
| 180 | 179 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘
𝐺)) |
| 181 | 30 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ) |
| 182 | 181 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → ℕ = dom ((,) ∘
𝐺)) |
| 183 | 182 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,)
∘ 𝐺)) |
| 184 | 129, 183 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺)) |
| 185 | | fvco 7007 |
. . . . 5
⊢ ((Fun
((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
| 186 | 180, 184,
185 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐺))‘𝑛) = (vol‘(((,) ∘
𝐺)‘𝑛))) |
| 187 | 168, 177,
186 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,)
∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘
𝐺))‘𝑛)) |
| 188 | 144, 163,
187 | eqfnfvd 7054 |
. 2
⊢ (𝜑 → (vol ∘ ((,) ∘
𝐹)) = (vol ∘ ((,)
∘ 𝐺))) |
| 189 | 125, 188 | jca 511 |
1
⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐺) ∧ (vol
∘ ((,) ∘ 𝐹)) =
(vol ∘ ((,) ∘ 𝐺)))) |