| Step | Hyp | Ref
| Expression |
| 1 | | rnco2 6273 |
. . 3
⊢ ran ([,]
∘ 𝐹) = ([,] “
ran 𝐹) |
| 2 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 3 | 2 | elin2d 4205 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ (ℝ ×
ℝ)) |
| 4 | | 1st2nd2 8053 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(𝐹‘𝑦) = 〈(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))〉) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) = 〈(1st ‘(𝐹‘𝑦)), (2nd ‘(𝐹‘𝑦))〉) |
| 6 | 5 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ([,]‘〈(1st
‘(𝐹‘𝑦)), (2nd
‘(𝐹‘𝑦))〉)) |
| 7 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) = ([,]‘〈(1st
‘(𝐹‘𝑦)), (2nd
‘(𝐹‘𝑦))〉) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) = ((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦)))) |
| 9 | | xp1st 8046 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑦)) ∈ ℝ) |
| 10 | 3, 9 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (1st
‘(𝐹‘𝑦)) ∈
ℝ) |
| 11 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑦) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑦)) ∈ ℝ) |
| 12 | 3, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → (2nd
‘(𝐹‘𝑦)) ∈
ℝ) |
| 13 | | iccssre 13469 |
. . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑦)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑦)) ∈ ℝ) →
((1st ‘(𝐹‘𝑦))[,](2nd ‘(𝐹‘𝑦))) ⊆ ℝ) |
| 14 | 10, 12, 13 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ((1st
‘(𝐹‘𝑦))[,](2nd
‘(𝐹‘𝑦))) ⊆
ℝ) |
| 15 | 8, 14 | eqsstrd 4018 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ⊆ ℝ) |
| 16 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 17 | 16 | elpw2 5334 |
. . . . . . 7
⊢
(([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ ↔
([,]‘(𝐹‘𝑦)) ⊆
ℝ) |
| 18 | 15, 17 | sylibr 234 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑦 ∈ ℕ) → ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ) |
| 19 | 18 | ralrimiva 3146 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∀𝑦 ∈ ℕ ([,]‘(𝐹‘𝑦)) ∈ 𝒫 ℝ) |
| 20 | | ffn 6736 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝐹 Fn ℕ) |
| 21 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → ([,]‘𝑥) = ([,]‘(𝐹‘𝑦))) |
| 22 | 21 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑦) → (([,]‘𝑥) ∈ 𝒫 ℝ ↔
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
| 23 | 22 | ralrn 7108 |
. . . . . 6
⊢ (𝐹 Fn ℕ →
(∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔
∀𝑦 ∈ ℕ
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
| 24 | 20, 23 | syl 17 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ ↔
∀𝑦 ∈ ℕ
([,]‘(𝐹‘𝑦)) ∈ 𝒫
ℝ)) |
| 25 | 19, 24 | mpbird 257 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ) |
| 26 | | iccf 13488 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 27 | | ffun 6739 |
. . . . . 6
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
| 28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ Fun
[,] |
| 29 | | frn 6743 |
. . . . . 6
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran 𝐹 ⊆ ( ≤ ∩ (ℝ ×
ℝ))) |
| 30 | | inss2 4238 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 31 | | rexpssxrxp 11306 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 32 | 30, 31 | sstri 3993 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 33 | 26 | fdmi 6747 |
. . . . . . 7
⊢ dom [,] =
(ℝ* × ℝ*) |
| 34 | 32, 33 | sseqtrri 4033 |
. . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ dom [,] |
| 35 | 29, 34 | sstrdi 3996 |
. . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran 𝐹 ⊆ dom [,]) |
| 36 | | funimass4 6973 |
. . . . 5
⊢ ((Fun [,]
∧ ran 𝐹 ⊆ dom
[,]) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔
∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)) |
| 37 | 28, 35, 36 | sylancr 587 |
. . . 4
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (([,] “ ran 𝐹) ⊆ 𝒫 ℝ ↔
∀𝑥 ∈ ran 𝐹([,]‘𝑥) ∈ 𝒫 ℝ)) |
| 38 | 25, 37 | mpbird 257 |
. . 3
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ([,] “ ran 𝐹) ⊆ 𝒫
ℝ) |
| 39 | 1, 38 | eqsstrid 4022 |
. 2
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ 𝒫
ℝ) |
| 40 | | sspwuni 5100 |
. 2
⊢ (ran ([,]
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ([,] ∘ 𝐹) ⊆
ℝ) |
| 41 | 39, 40 | sylib 218 |
1
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |