| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elee 28909 | . 2
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ)) | 
| 2 |  | ovex 7464 | . . . . 5
⊢ (𝐴𝐹𝐵) ∈ V | 
| 3 |  | eqid 2737 | . . . . 5
⊢ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) = (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) | 
| 4 | 2, 3 | fnmpti 6711 | . . . 4
⊢ (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) Fn (1...𝑁) | 
| 5 |  | df-f 6565 | . . . 4
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) Fn (1...𝑁) ∧ ran (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ)) | 
| 6 | 4, 5 | mpbiran 709 | . . 3
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ran (𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ) | 
| 7 | 3 | rnmpt 5968 | . . . . 5
⊢ ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) = {𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} | 
| 8 | 7 | sseq1i 4012 | . . . 4
⊢ (ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ ↔ {𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ) | 
| 9 |  | abss 4063 | . . . . 5
⊢ ({𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ ↔ ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 10 |  | nfre1 3285 | . . . . . . . . 9
⊢
Ⅎ𝑘∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) | 
| 11 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑘 𝑎 ∈ ℝ | 
| 12 | 10, 11 | nfim 1896 | . . . . . . . 8
⊢
Ⅎ𝑘(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) | 
| 13 | 12 | nfal 2323 | . . . . . . 7
⊢
Ⅎ𝑘∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) | 
| 14 |  | r19.23v 3183 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ (∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 15 | 14 | albii 1819 | . . . . . . . 8
⊢
(∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 16 |  | ralcom4 3286 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 17 |  | rsp 3247 | . . . . . . . . . 10
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → ∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ))) | 
| 18 | 2 | clel2 3660 | . . . . . . . . . 10
⊢ ((𝐴𝐹𝐵) ∈ ℝ ↔ ∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 19 | 17, 18 | imbitrrdi 252 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)∀𝑎(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) | 
| 20 | 16, 19 | sylbir 235 | . . . . . . . 8
⊢
(∀𝑎∀𝑘 ∈ (1...𝑁)(𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) | 
| 21 | 15, 20 | sylbir 235 | . . . . . . 7
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) | 
| 22 | 13, 21 | ralrimi 3257 | . . . . . 6
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) → ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) | 
| 23 |  | nfra1 3284 | . . . . . . . 8
⊢
Ⅎ𝑘∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ | 
| 24 |  | rsp 3247 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (𝑘 ∈ (1...𝑁) → (𝐴𝐹𝐵) ∈ ℝ)) | 
| 25 |  | eleq1a 2836 | . . . . . . . . 9
⊢ ((𝐴𝐹𝐵) ∈ ℝ → (𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 26 | 24, 25 | syl6 35 | . . . . . . . 8
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (𝑘 ∈ (1...𝑁) → (𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ))) | 
| 27 | 23, 11, 26 | rexlimd 3266 | . . . . . . 7
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → (∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 28 | 27 | alrimiv 1927 | . . . . . 6
⊢
(∀𝑘 ∈
(1...𝑁)(𝐴𝐹𝐵) ∈ ℝ → ∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ)) | 
| 29 | 22, 28 | impbii 209 | . . . . 5
⊢
(∀𝑎(∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵) → 𝑎 ∈ ℝ) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) | 
| 30 | 9, 29 | bitri 275 | . . . 4
⊢ ({𝑎 ∣ ∃𝑘 ∈ (1...𝑁)𝑎 = (𝐴𝐹𝐵)} ⊆ ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) | 
| 31 | 8, 30 | bitri 275 | . . 3
⊢ (ran
(𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ⊆ ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) | 
| 32 | 6, 31 | bitri 275 | . 2
⊢ ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)):(1...𝑁)⟶ℝ ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ) | 
| 33 | 1, 32 | bitrdi 287 | 1
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (𝐴𝐹𝐵)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(𝐴𝐹𝐵) ∈ ℝ)) |