Proof of Theorem uniioombllem3a
| Step | Hyp | Ref
| Expression |
| 1 | | uniioombl.k |
. . 3
⊢ 𝐾 = ∪
(((,) ∘ 𝐺) “
(1...𝑀)) |
| 2 | | ioof 13487 |
. . . . . 6
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 3 | | uniioombl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 4 | | inss2 4238 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 5 | | rexpssxrxp 11306 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 6 | 4, 5 | sstri 3993 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 7 | | fss 6752 |
. . . . . . 7
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 8 | 3, 6, 7 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* ×
ℝ*)) |
| 9 | | fco 6760 |
. . . . . 6
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐺:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 10 | 2, 8, 9 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫
ℝ) |
| 11 | | ffun 6739 |
. . . . 5
⊢ (((,)
∘ 𝐺):ℕ⟶𝒫 ℝ →
Fun ((,) ∘ 𝐺)) |
| 12 | | funiunfv 7268 |
. . . . 5
⊢ (Fun ((,)
∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
| 13 | 10, 11, 12 | 3syl 18 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,)
∘ 𝐺) “
(1...𝑀))) |
| 14 | | elfznn 13593 |
. . . . . 6
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
| 15 | | fvco3 7008 |
. . . . . 6
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
| 16 | 3, 14, 15 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗))) |
| 17 | 16 | iuneq2dv 5016 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 18 | 13, 17 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪
𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 19 | 1, 18 | eqtrid 2789 |
. 2
⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) |
| 20 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 21 | 3, 14, 20 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 22 | 21 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ ×
ℝ)) |
| 23 | | 1st2nd2 8053 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) →
(𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = 〈(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))〉) |
| 25 | 24 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉)) |
| 26 | | df-ov 7434 |
. . . . . . . 8
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘〈(1st
‘(𝐺‘𝑗)), (2nd
‘(𝐺‘𝑗))〉) |
| 27 | 25, 26 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗)))) |
| 28 | | ioossre 13448 |
. . . . . . 7
⊢
((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ |
| 29 | 27, 28 | eqsstrdi 4028 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 30 | 29 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 31 | | iunss 5045 |
. . . . 5
⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 32 | 30, 31 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ) |
| 33 | 19, 32 | eqsstrd 4018 |
. . 3
⊢ (𝜑 → 𝐾 ⊆ ℝ) |
| 34 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 35 | 27 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗))))) |
| 36 | | ovolfcl 25501 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st
‘(𝐺‘𝑗)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑗)) ≤ (2nd
‘(𝐺‘𝑗)))) |
| 37 | 3, 14, 36 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗)))) |
| 38 | | ovolioo 25603 |
. . . . . . 7
⊢
(((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑗)) ∈ ℝ ∧
(1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((1st
‘(𝐺‘𝑗))(,)(2nd
‘(𝐺‘𝑗)))) = ((2nd
‘(𝐺‘𝑗)) − (1st
‘(𝐺‘𝑗)))) |
| 40 | 35, 39 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) |
| 41 | 37 | simp2d 1144 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ) |
| 42 | 37 | simp1d 1143 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ) |
| 43 | 41, 42 | resubcld 11691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ) |
| 44 | 40, 43 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 45 | 34, 44 | fsumrecl 15770 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ) |
| 46 | 19 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (vol*‘𝐾) = (vol*‘∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))) |
| 47 | 29, 44 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)) |
| 48 | 47 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)) |
| 49 | | ovolfiniun 25536 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ∀𝑗 ∈
(1...𝑀)(((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧
(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)) →
(vol*‘∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗)))) |
| 50 | 34, 48, 49 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗)))) |
| 51 | 46, 50 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → (vol*‘𝐾) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗)))) |
| 52 | | ovollecl 25518 |
. . 3
⊢ ((𝐾 ⊆ ℝ ∧
Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ ∧ (vol*‘𝐾) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘((,)‘(𝐺‘𝑗)))) → (vol*‘𝐾) ∈ ℝ) |
| 53 | 33, 45, 51, 52 | syl3anc 1373 |
. 2
⊢ (𝜑 → (vol*‘𝐾) ∈
ℝ) |
| 54 | 19, 53 | jca 511 |
1
⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ)) |