Proof of Theorem uniioombllem2a
| Step | Hyp | Ref
| Expression |
| 1 | | uniioombl.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 3 | 2 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 4 | 3 | elin2d 4205 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ (ℝ ×
ℝ)) |
| 5 | | 1st2nd2 8053 |
. . . . . . 7
⊢ ((𝐹‘𝑧) ∈ (ℝ × ℝ) →
(𝐹‘𝑧) = 〈(1st ‘(𝐹‘𝑧)), (2nd ‘(𝐹‘𝑧))〉) |
| 6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) = 〈(1st ‘(𝐹‘𝑧)), (2nd ‘(𝐹‘𝑧))〉) |
| 7 | 6 | fveq2d 6910 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐹‘𝑧)) = ((,)‘〈(1st
‘(𝐹‘𝑧)), (2nd
‘(𝐹‘𝑧))〉)) |
| 8 | | df-ov 7434 |
. . . . 5
⊢
((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) = ((,)‘〈(1st
‘(𝐹‘𝑧)), (2nd
‘(𝐹‘𝑧))〉) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐹‘𝑧)) = ((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧)))) |
| 10 | | uniioombl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 11 | 10 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 12 | 11 | elin2d 4205 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) ∈ (ℝ ×
ℝ)) |
| 13 | | 1st2nd2 8053 |
. . . . . . . 8
⊢ ((𝐺‘𝐽) ∈ (ℝ × ℝ) →
(𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (𝐺‘𝐽) = 〈(1st ‘(𝐺‘𝐽)), (2nd ‘(𝐺‘𝐽))〉) |
| 15 | 14 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉)) |
| 16 | | df-ov 7434 |
. . . . . 6
⊢
((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))) = ((,)‘〈(1st
‘(𝐺‘𝐽)), (2nd
‘(𝐺‘𝐽))〉) |
| 17 | 15, 16 | eqtr4di 2795 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((,)‘(𝐺‘𝐽)) = ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) |
| 19 | 9, 18 | ineq12d 4221 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) ∩ ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽))))) |
| 20 | | ovolfcl 25501 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑧 ∈ ℕ) → ((1st
‘(𝐹‘𝑧)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐹‘𝑧)))) |
| 21 | 2, 20 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → ((1st
‘(𝐹‘𝑧)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐹‘𝑧)))) |
| 22 | 21 | simp1d 1143 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐹‘𝑧)) ∈
ℝ) |
| 23 | 22 | rexrd 11311 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐹‘𝑧)) ∈
ℝ*) |
| 24 | 21 | simp2d 1144 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐹‘𝑧)) ∈
ℝ) |
| 25 | 24 | rexrd 11311 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐹‘𝑧)) ∈
ℝ*) |
| 26 | | ovolfcl 25501 |
. . . . . . . 8
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
| 27 | 10, 26 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → ((1st
‘(𝐺‘𝐽)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ ∧ (1st
‘(𝐺‘𝐽)) ≤ (2nd
‘(𝐺‘𝐽)))) |
| 28 | 27 | simp1d 1143 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ) |
| 29 | 28 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ*) |
| 30 | 29 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (1st
‘(𝐺‘𝐽)) ∈
ℝ*) |
| 31 | 27 | simp2d 1144 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ) |
| 32 | 31 | rexrd 11311 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ*) |
| 33 | 32 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (2nd
‘(𝐺‘𝐽)) ∈
ℝ*) |
| 34 | | iooin 13421 |
. . . 4
⊢
((((1st ‘(𝐹‘𝑧)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑧)) ∈ ℝ*) ∧
((1st ‘(𝐺‘𝐽)) ∈ ℝ* ∧
(2nd ‘(𝐺‘𝐽)) ∈ ℝ*)) →
(((1st ‘(𝐹‘𝑧))(,)(2nd ‘(𝐹‘𝑧))) ∩ ((1st ‘(𝐺‘𝐽))(,)(2nd ‘(𝐺‘𝐽)))) = (if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽))))) |
| 35 | 23, 25, 30, 33, 34 | syl22anc 839 |
. . 3
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((1st
‘(𝐹‘𝑧))(,)(2nd
‘(𝐹‘𝑧))) ∩ ((1st
‘(𝐺‘𝐽))(,)(2nd
‘(𝐺‘𝐽)))) = (if((1st
‘(𝐹‘𝑧)) ≤ (1st
‘(𝐺‘𝐽)), (1st
‘(𝐺‘𝐽)), (1st
‘(𝐹‘𝑧)))(,)if((2nd
‘(𝐹‘𝑧)) ≤ (2nd
‘(𝐺‘𝐽)), (2nd
‘(𝐹‘𝑧)), (2nd
‘(𝐺‘𝐽))))) |
| 36 | 19, 35 | eqtrd 2777 |
. 2
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) = (if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽))))) |
| 37 | | ioorebas 13491 |
. 2
⊢
(if((1st ‘(𝐹‘𝑧)) ≤ (1st ‘(𝐺‘𝐽)), (1st ‘(𝐺‘𝐽)), (1st ‘(𝐹‘𝑧)))(,)if((2nd ‘(𝐹‘𝑧)) ≤ (2nd ‘(𝐺‘𝐽)), (2nd ‘(𝐹‘𝑧)), (2nd ‘(𝐺‘𝐽)))) ∈ ran (,) |
| 38 | 36, 37 | eqeltrdi 2849 |
1
⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) |