Metamath Proof Explorer

Theorem chlimi

Description: The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypothesis chlim.1 ⊢ A ∈ V
Assertion chlimi ⊢ H ∈ C ℋ ∧ F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H

Proof

Step Hyp Ref Expression
1 chlim.1 ⊢ A ∈ V
2 isch2 ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
3 2 simprbi ⊢ H ∈ C ℋ → ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
4 nnex ⊢ ℕ ∈ V
5 fex ⊢ F : ℕ ⟶ H ∧ ℕ ∈ V → F ∈ V
6 4 5 mpan2 ⊢ F : ℕ ⟶ H → F ∈ V
7 6 adantr ⊢ F : ℕ ⟶ H ∧ F ⇝v A → F ∈ V
8 feq1 ⊢ f = F → f : ℕ ⟶ H ↔ F : ℕ ⟶ H
9 breq1 ⊢ f = F → f ⇝v x ↔ F ⇝v x
10 8 9 anbi12d ⊢ f = F → f : ℕ ⟶ H ∧ f ⇝v x ↔ F : ℕ ⟶ H ∧ F ⇝v x
11 10 imbi1d ⊢ f = F → f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H ↔ F : ℕ ⟶ H ∧ F ⇝v x → x ∈ H
12 11 albidv ⊢ f = F → ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H ↔ ∀ x F : ℕ ⟶ H ∧ F ⇝v x → x ∈ H
13 12 spcgv ⊢ F ∈ V → ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H → ∀ x F : ℕ ⟶ H ∧ F ⇝v x → x ∈ H
14 breq2 ⊢ x = A → F ⇝v x ↔ F ⇝v A
15 14 anbi2d ⊢ x = A → F : ℕ ⟶ H ∧ F ⇝v x ↔ F : ℕ ⟶ H ∧ F ⇝v A
16 eleq1 ⊢ x = A → x ∈ H ↔ A ∈ H
17 15 16 imbi12d ⊢ x = A → F : ℕ ⟶ H ∧ F ⇝v x → x ∈ H ↔ F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
18 1 17 spcv ⊢ ∀ x F : ℕ ⟶ H ∧ F ⇝v x → x ∈ H → F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
19 13 18 syl6 ⊢ F ∈ V → ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H → F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
20 7 19 syl ⊢ F : ℕ ⟶ H ∧ F ⇝v A → ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H → F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
21 20 pm2.43b ⊢ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H → F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
22 3 21 syl ⊢ H ∈ C ℋ → F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H
23 22 3impib ⊢ H ∈ C ℋ ∧ F : ℕ ⟶ H ∧ F ⇝v A → A ∈ H