Step | Hyp | Ref
| Expression |
1 | | rnco2 6157 |
. . 3
⊢ ran ([,]
∘ 𝐹) = ([,] “
ran 𝐹) |
2 | | ffvelrn 6959 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
3 | 2 | elin2d 4133 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ (ℝ ×
ℝ)) |
4 | | 1st2nd2 7870 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(𝐹‘𝑦) = 〈(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))〉) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) = 〈(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))〉) |
6 | 5 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ([,]‘〈(1st
‘(𝐹‘𝑦)), (2nd
‘(𝐹‘𝑦))〉)) |
7 | | df-ov 7278 |
. . . . . . . . 9
⊢
((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) = ([,]‘〈(1st
‘(𝐹‘𝑦)), (2nd
‘(𝐹‘𝑦))〉) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦)))) |
9 | | xp1st 7863 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑦)) ∈ ℝ) |
10 | 3, 9 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (1st
‘(𝐹‘𝑦)) ∈
ℝ) |
11 | | xp2nd 7864 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑦)) ∈ ℝ) |
12 | 3, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (2nd
‘(𝐹‘𝑦)) ∈
ℝ) |
13 | | iccssre 13161 |
. . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑦)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑦)) ∈ ℝ) →
((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) ⊆ ℝ) |
14 | 10, 12, 13 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ((1st
‘(𝐹‘𝑦))[,](2nd
‘(𝐹‘𝑦))) ⊆
ℝ) |
15 | 8, 14 | eqsstrd 3959 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ⊆ ℝ) |
16 | | reex 10962 |
. . . . . . . 8
⊢ ℝ
∈ V |
17 | 16 | elpw2 5269 |
. . . . . . 7
⊢
(([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ ↔
([,]‘(𝐹‘𝑦)) ⊆
ℝ) |
18 | 15, 17 | sylibr 233 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ) |
19 | 18 | ralrimiva 3103 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∀𝑦 ∈ ℕ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ) |
20 | | ffn 6600 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝐹 Fn ℕ) |
21 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → ([,]‘𝑥) = ([,]‘(𝐹‘𝑦))) |
22 | 21 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑦) → (([,]‘𝑥) ∈ 𝒫 ℝ ↔
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
23 | 22 | ralrn 6964 |
. . . . . 6
⊢ (𝐹 Fn ℕ →
(∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔
∀𝑦 ∈ ℕ
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
24 | 20, 23 | syl 17 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔
∀𝑦 ∈ ℕ
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
25 | 19, 24 | mpbird 256 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ) |
26 | | iccf 13180 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
27 | | ffun 6603 |
. . . . . 6
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ Fun
[,] |
29 | | frn 6607 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran 𝐹 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) |
30 | | inss2 4163 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
31 | | rexpssxrxp 11020 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
32 | 30, 31 | sstri 3930 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
33 | 26 | fdmi 6612 |
. . . . . . 7
⊢ dom [,] =
(ℝ* × ℝ*) |
34 | 32, 33 | sseqtrri 3958 |
. . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ dom [,] |
35 | 29, 34 | sstrdi 3933 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran 𝐹 ⊆ dom [,]) |
36 | | funimass4 6834 |
. . . . 5
⊢ ((Fun [,]
∧ ran 𝐹 ⊆ dom
[,]) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔
∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)) |
37 | 28, 35, 36 | sylancr 587 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔
∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)) |
38 | 25, 37 | mpbird 256 |
. . 3
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ([,] “ ran 𝐹) ⊆ 𝒫
ℝ) |
39 | 1, 38 | eqsstrid 3969 |
. 2
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ 𝒫
ℝ) |
40 | | sspwuni 5029 |
. 2
⊢ (ran ([,]
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ([,] ∘ 𝐹) ⊆
ℝ) |
41 | 39, 40 | sylib 217 |
1
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |