Step | Hyp | Ref
| Expression |
1 | | elee 27262 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ)) |
2 | | ovex 7308 |
. . . . 5
⊢ (𝐴𝐹𝐵) ∈ V |
3 | | eqid 2738 |
. . . . 5
⊢ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) = (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) |
4 | 2, 3 | fnmpti 6576 |
. . . 4
⊢ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) Fn (1...𝑁) |
5 | | df-f 6437 |
. . . 4
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) Fn (1...𝑁) ∧ ran (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ)) |
6 | 4, 5 | mpbiran 706 |
. . 3
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ran (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ) |
7 | 3 | rnmpt 5864 |
. . . . 5
⊢ ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) = {𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} |
8 | 7 | sseq1i 3949 |
. . . 4
⊢ (ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ ↔ {𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ) |
9 | | abss 3994 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ ↔ ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
10 | | nfre1 3239 |
. . . . . . . . 9
⊢
Ⅎ𝑘∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) |
11 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑎 ∈ ℝ |
12 | 10, 11 | nfim 1899 |
. . . . . . . 8
⊢
Ⅎ𝑘(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) |
13 | 12 | nfal 2317 |
. . . . . . 7
⊢
Ⅎ𝑘∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) |
14 | | r19.23v 3208 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ (∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
15 | 14 | albii 1822 |
. . . . . . . 8
⊢
(∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
16 | | ralcom4 3164 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
17 | | rsp 3131 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → ∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ))) |
18 | 2 | clel2 3590 |
. . . . . . . . . 10
⊢ ((𝐴𝐹𝐵) ∈ ℝ ↔ ∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
19 | 17, 18 | syl6ibr 251 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) |
20 | 16, 19 | sylbir 234 |
. . . . . . . 8
⊢
(∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) |
21 | 15, 20 | sylbir 234 |
. . . . . . 7
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) |
22 | 13, 21 | ralrimi 3141 |
. . . . . 6
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) |
23 | | nfra1 3144 |
. . . . . . . 8
⊢
Ⅎ𝑘∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ |
24 | | rsp 3131 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) |
25 | | eleq1a 2834 |
. . . . . . . . 9
⊢ ((𝐴𝐹𝐵) ∈ ℝ → (𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
26 | 24, 25 | syl6 35 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (𝑘 ∈ (1...𝑁) → (𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ))) |
27 | 23, 11, 26 | rexlimd 3250 |
. . . . . . 7
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
28 | 27 | alrimiv 1930 |
. . . . . 6
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) |
29 | 22, 28 | impbii 208 |
. . . . 5
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) |
30 | 9, 29 | bitri 274 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) |
31 | 8, 30 | bitri 274 |
. . 3
⊢ (ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) |
32 | 6, 31 | bitri 274 |
. 2
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) |
33 | 1, 32 | bitrdi 287 |
1
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ)) |