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 ⊢ 𝐴 ∈ V
Assertion chlimi ( ( 𝐻 ∈ Cℋ ∧ 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝𝑣 𝐴 ) → 𝐴 ∈ 𝐻 )

Proof

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