Proof of Theorem ovolficc
Step | Hyp | Ref
| Expression |
1 | | iccf 12272 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
2 | | inss2 3834 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
3 | | rexpssxrxp 10084 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
4 | 2, 3 | sstri 3612 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
5 | | fss 6056 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
6 | 4, 5 | mpan2 707 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
7 | | fco 6058 |
. . . . . 6
⊢
(([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ([,] ∘ 𝐹):ℕ⟶𝒫
ℝ*) |
8 | 1, 6, 7 | sylancr 695 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ([,] ∘ 𝐹):ℕ⟶𝒫
ℝ*) |
9 | | ffn 6045 |
. . . . 5
⊢ (([,]
∘ 𝐹):ℕ⟶𝒫
ℝ* → ([,] ∘ 𝐹) Fn ℕ) |
10 | | fniunfv 6505 |
. . . . 5
⊢ (([,]
∘ 𝐹) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (([,] ∘ 𝐹)‘𝑛) = ∪ ran ([,]
∘ 𝐹)) |
11 | 8, 9, 10 | 3syl 18 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ 𝑛 ∈ ℕ (([,] ∘
𝐹)‘𝑛) = ∪ ran ([,]
∘ 𝐹)) |
12 | 11 | sseq2d 3633 |
. . 3
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹))) |
13 | 12 | adantl 482 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹))) |
14 | | dfss3 3592 |
. . 3
⊢ (𝐴 ⊆ ∪ 𝑛 ∈ ℕ (([,] ∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 𝑧 ∈ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛)) |
15 | | ssel2 3598 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
16 | | eliun 4524 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑛 ∈ ℕ (([,] ∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ 𝑧 ∈ (([,] ∘ 𝐹)‘𝑛)) |
17 | | fvco3 6275 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑛) = ([,]‘(𝐹‘𝑛))) |
18 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
19 | 2, 18 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ ×
ℝ)) |
20 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ (ℝ × ℝ) →
(𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
22 | 21 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ([,]‘(𝐹‘𝑛)) = ([,]‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
23 | | df-ov 6653 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛))) = ([,]‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ([,]‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛)))) |
25 | 17, 24 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (([,] ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛)))) |
26 | 25 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (([,] ∘ 𝐹)‘𝑛) ↔ 𝑧 ∈ ((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛))))) |
27 | | ovolfcl 23235 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
28 | | elicc2 12238 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ) → (𝑧 ∈ ((1st
‘(𝐹‘𝑛))[,](2nd
‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
29 | | 3anass 1042 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧
(1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
30 | 28, 29 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ) → (𝑧 ∈ ((1st
‘(𝐹‘𝑛))[,](2nd
‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
31 | 30 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → (𝑧 ∈ ((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
32 | 27, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ((1st ‘(𝐹‘𝑛))[,](2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
33 | 26, 32 | bitrd 268 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (([,] ∘ 𝐹)‘𝑛) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
34 | 33 | adantll 750 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (([,] ∘ 𝐹)‘𝑛) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
35 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℝ) |
36 | 35 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ ∧ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))) |
37 | 34, 36 | bitr4d 271 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (([,] ∘ 𝐹)‘𝑛) ↔ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
38 | 37 | rexbidva 3049 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (∃𝑛 ∈ ℕ 𝑧 ∈ (([,] ∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
39 | 16, 38 | syl5bb 272 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
40 | 15, 39 | sylan 488 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
41 | 40 | an32s 846 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
42 | 41 | ralbidva 2985 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (∀𝑧 ∈ 𝐴 𝑧 ∈ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
43 | 14, 42 | syl5bb 272 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (([,]
∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |
44 | 13, 43 | bitr3d 270 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
([,] ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) |