Proof of Theorem uniioombllem2a
Step | Hyp | Ref
| Expression |
1 | | inss2 4053 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
2 | | uniioombl.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
3 | 2 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
4 | 3 | ffvelrnda 6623 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
5 | 1, 4 | sseldi 3818 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ (ℝ ×
ℝ)) |
6 | | 1st2nd2 7484 |
. . . . . . 7
⊢ ((𝐹‘𝑧) ∈ (ℝ × ℝ) →
(𝐹‘𝑧) = 〈(1st ‘(𝐹‘𝑧)), (2nd ‘(𝐹‘𝑧))〉) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) = 〈(1st ‘(𝐹‘𝑧)), (2nd ‘(𝐹‘𝑧))〉) |
8 | 7 | fveq2d 6450 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐹‘𝑧)) = ((,)‘〈(1st
‘(𝐹‘𝑧)), (2nd
‘(𝐹‘𝑧))〉)) |
9 | | df-ov 6925 |
. . . . 5
⊢
((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) = ((,)‘〈(1st
‘(𝐹‘𝑧)), (2nd
‘(𝐹‘𝑧))〉) |
10 | 8, 9 | syl6eqr 2831 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐹‘𝑧)) = ((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧)))) |
11 | | uniioombl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
12 | 11 | ffvelrnda 6623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
13 | 1, 12 | sseldi 3818 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ (ℝ ×
ℝ)) |
14 | | 1st2nd2 7484 |
. . . . . . . 8
⊢ ((𝐺‘𝐽) ∈ (ℝ × ℝ) →
(𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
16 | 15 | fveq2d 6450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉)) |
17 | | df-ov 6925 |
. . . . . 6
⊢
((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉) |
18 | 16, 17 | syl6eqr 2831 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) |
19 | 18 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) |
20 | 10, 19 | ineq12d 4037 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) ∩ ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))))) |
21 | | ovolfcl 23670 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑧 ∈ ℕ) → ((1st
‘(𝐹‘𝑧)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐹‘𝑧)))) |
22 | 3, 21 | sylan 575 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((1st
‘(𝐹‘𝑧)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐹‘𝑧)))) |
23 | 22 | simp1d 1133 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐹‘𝑧)) ∈
ℝ) |
24 | 23 | rexrd 10426 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐹‘𝑧)) ∈
ℝ*) |
25 | 22 | simp2d 1134 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐹‘𝑧)) ∈
ℝ) |
26 | 25 | rexrd 10426 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐹‘𝑧)) ∈
ℝ*) |
27 | | ovolfcl 23670 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
28 | 11, 27 | sylan 575 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
29 | 28 | simp1d 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ) |
30 | 29 | rexrd 10426 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ*) |
31 | 30 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ*) |
32 | 28 | simp2d 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ) |
33 | 32 | rexrd 10426 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ*) |
34 | 33 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ*) |
35 | | iooin 12521 |
. . . 4
⊢
((((1st ‘(𝐹‘𝑧)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ*) ∧
((1st ‘(𝐺‘𝐽)) ∈ ℝ* ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ*)) →
(((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) ∩ ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) = (if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽))))) |
36 | 24, 26, 31, 34, 35 | syl22anc 829 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((1st
‘(𝐹‘𝑧))(,)(2nd
‘(𝐹‘𝑧))) ∩ ((1st
‘(𝐺‘𝐽))(,)(2nd
‘(𝐺‘𝐽)))) = (if((1st
‘(𝐹‘𝑧)) ≤ (1st
‘(𝐺‘𝐽)), (1st
‘(𝐺‘𝐽)), (1st
‘(𝐹‘𝑧)))(,)if((2nd
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐺‘𝐽)), (2nd
‘(𝐹‘𝑧)), (2nd
‘(𝐺‘𝐽))))) |
37 | 20, 36 | eqtrd 2813 |
. 2
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽))))) |
38 | | ioorebas 12588 |
. 2
⊢
(if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽)))) ∈ ran (,) |
39 | 37, 38 | syl6eqel 2866 |
1
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) |