Step |
Hyp |
Ref |
Expression |
1 |
|
iccf |
⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |
2 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
3 |
|
rexpssxrxp |
⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) |
4 |
2 3
|
sstri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) |
5 |
|
fss |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
6 |
4 5
|
mpan2 |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
7 |
|
fco |
⊢ ( ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* ) |
8 |
1 6 7
|
sylancr |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* ) |
9 |
|
ffn |
⊢ ( ( [,] ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ* → ( [,] ∘ 𝐹 ) Fn ℕ ) |
10 |
|
fniunfv |
⊢ ( ( [,] ∘ 𝐹 ) Fn ℕ → ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ∪ ran ( [,] ∘ 𝐹 ) ) |
11 |
8 9 10
|
3syl |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ∪ ran ( [,] ∘ 𝐹 ) ) |
12 |
11
|
sseq2d |
⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( 𝐴 ⊆ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ) |
14 |
|
dfss3 |
⊢ ( 𝐴 ⊆ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ) |
15 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ ) |
16 |
|
eliun |
⊢ ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ) |
17 |
|
simpll |
⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℝ ) |
18 |
|
fvco3 |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ( [,] ‘ ( 𝐹 ‘ 𝑛 ) ) ) |
19 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
20 |
19
|
elin2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) ) |
21 |
|
1st2nd2 |
⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑛 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
22 |
20 21
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑛 ) ) = ( [,] ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) ) |
24 |
|
df-ov |
⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( [,] ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
25 |
23 24
|
eqtr4di |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( [,] ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
26 |
18 25
|
eqtrd |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
27 |
26
|
eleq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 ∈ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
28 |
|
ovolfcl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
29 |
|
elicc2 |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
30 |
|
3anass |
⊢ ( ( 𝑧 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
31 |
29 30
|
bitrdi |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) |
32 |
31
|
3adant3 |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) |
33 |
28 32
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) [,] ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) |
34 |
27 33
|
bitrd |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) |
35 |
34
|
adantll |
⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) ) |
36 |
17 35
|
mpbirand |
⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
37 |
36
|
rexbidva |
⊢ ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∃ 𝑛 ∈ ℕ 𝑧 ∈ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
38 |
16 37
|
syl5bb |
⊢ ( ( 𝑧 ∈ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
39 |
15 38
|
sylan |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
40 |
39
|
an32s |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
41 |
40
|
ralbidva |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ∀ 𝑧 ∈ 𝐴 𝑧 ∈ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
42 |
14 41
|
syl5bb |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ 𝑛 ∈ ℕ ( ( [,] ∘ 𝐹 ) ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
43 |
13 42
|
bitr3d |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |