Proof of Theorem ovolfioo
| Step | Hyp | Ref
| Expression |
| 1 | | ioof 13487 |
. . . . . 6
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 2 | | inss2 4238 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 3 | | rexpssxrxp 11306 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 4 | 2, 3 | sstri 3993 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 5 | | fss 6752 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 6 | 4, 5 | mpan2 691 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 7 | | fco 6760 |
. . . . . 6
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 8 | 1, 6, 7 | sylancr 587 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 9 | | ffn 6736 |
. . . . 5
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
((,) ∘ 𝐹) Fn
ℕ) |
| 10 | | fniunfv 7267 |
. . . . 5
⊢ (((,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
| 11 | 8, 9, 10 | 3syl 18 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ 𝑛 ∈ ℕ (((,) ∘
𝐹)‘𝑛) = ∪ ran ((,)
∘ 𝐹)) |
| 12 | 11 | sseq2d 4016 |
. . 3
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹))) |
| 13 | 12 | adantl 481 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹))) |
| 14 | | dfss3 3972 |
. . 3
⊢ (𝐴 ⊆ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 𝑧 ∈ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛)) |
| 15 | | ssel2 3978 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
| 16 | | eliun 4995 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ 𝑧 ∈ (((,) ∘ 𝐹)‘𝑛)) |
| 17 | | rexr 11307 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℝ*) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℝ*) |
| 19 | | fvco3 7008 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛))) |
| 20 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 21 | 20 | elin2d 4205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ ×
ℝ)) |
| 22 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ (ℝ × ℝ) →
(𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
| 24 | 23 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉)) |
| 25 | | df-ov 7434 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘〈(1st
‘(𝐹‘𝑛)), (2nd
‘(𝐹‘𝑛))〉) |
| 26 | 24, 25 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 27 | 19, 26 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (((,) ∘ 𝐹)‘𝑛) ↔ 𝑧 ∈ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))) |
| 29 | | ovolfcl 25501 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
| 30 | | rexr 11307 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑛)) ∈ ℝ → (1st
‘(𝐹‘𝑛)) ∈
ℝ*) |
| 31 | | rexr 11307 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(𝐹‘𝑛)) ∈ ℝ → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
| 32 | | elioo1 13427 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ*) → (𝑧 ∈ ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
(1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ) → (𝑧 ∈ ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
(1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 34 | | 3anass 1095 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ*
∧ (1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 35 | 33, 34 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ) → (𝑧 ∈ ((1st
‘(𝐹‘𝑛))(,)(2nd
‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))) |
| 36 | 35 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ ∧
(1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → (𝑧 ∈ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))) |
| 37 | 29, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))) |
| 38 | 28, 37 | bitrd 279 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (((,) ∘ 𝐹)‘𝑛) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))) |
| 39 | 38 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (((,) ∘ 𝐹)‘𝑛) ↔ (𝑧 ∈ ℝ* ∧
((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))) |
| 40 | 18, 39 | mpbirand 707 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ (((,) ∘ 𝐹)‘𝑛) ↔ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 41 | 40 | rexbidva 3177 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (∃𝑛 ∈ ℕ 𝑧 ∈ (((,) ∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 42 | 16, 41 | bitrid 283 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 43 | 15, 42 | sylan 580 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 44 | 43 | an32s 652 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 45 | 44 | ralbidva 3176 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (∀𝑧 ∈ 𝐴 𝑧 ∈ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 46 | 14, 45 | bitrid 283 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪
𝑛 ∈ ℕ (((,)
∘ 𝐹)‘𝑛) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |
| 47 | 13, 46 | bitr3d 281 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) |