Step |
Hyp |
Ref |
Expression |
1 |
|
rnco2 |
⊢ ran ( [,] ∘ 𝐹 ) = ( [,] “ ran 𝐹 ) |
2 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
3 |
2
|
elin2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) ) |
4 |
|
1st2nd2 |
⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑦 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) 〉 ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) 〉 ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) = ( [,] ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) 〉 ) ) |
7 |
|
df-ov |
⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( [,] ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) 〉 ) |
8 |
6 7
|
eqtr4di |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) |
9 |
|
xp1st |
⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) |
10 |
3 9
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) |
11 |
|
xp2nd |
⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) |
12 |
3 11
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) |
13 |
|
iccssre |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⊆ ℝ ) |
14 |
10 12 13
|
syl2anc |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑦 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⊆ ℝ ) |
15 |
8 14
|
eqsstrd |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ ) |
16 |
|
reex |
⊢ ℝ ∈ V |
17 |
16
|
elpw2 |
⊢ ( ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ↔ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ ) |
18 |
15 17
|
sylibr |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑦 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) |
19 |
18
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) |
20 |
|
ffn |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ℕ ) |
21 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( [,] ‘ 𝑥 ) = ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ) |
22 |
21
|
eleq1d |
⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) ) |
23 |
22
|
ralrn |
⊢ ( 𝐹 Fn ℕ → ( ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) ) |
24 |
20 23
|
syl |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ↔ ∀ 𝑦 ∈ ℕ ( [,] ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝒫 ℝ ) ) |
25 |
19 24
|
mpbird |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ) |
26 |
|
iccf |
⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |
27 |
|
ffun |
⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] ) |
28 |
26 27
|
ax-mp |
⊢ Fun [,] |
29 |
|
frn |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
30 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
31 |
|
rexpssxrxp |
⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) |
32 |
30 31
|
sstri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) |
33 |
26
|
fdmi |
⊢ dom [,] = ( ℝ* × ℝ* ) |
34 |
32 33
|
sseqtrri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ dom [,] |
35 |
29 34
|
sstrdi |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ dom [,] ) |
36 |
|
funimass4 |
⊢ ( ( Fun [,] ∧ ran 𝐹 ⊆ dom [,] ) → ( ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ) ) |
37 |
28 35 36
|
sylancr |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ ran 𝐹 ( [,] ‘ 𝑥 ) ∈ 𝒫 ℝ ) ) |
38 |
25 37
|
mpbird |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( [,] “ ran 𝐹 ) ⊆ 𝒫 ℝ ) |
39 |
1 38
|
eqsstrid |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran ( [,] ∘ 𝐹 ) ⊆ 𝒫 ℝ ) |
40 |
|
sspwuni |
⊢ ( ran ( [,] ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ ) |
41 |
39 40
|
sylib |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ ) |