Metamath Proof Explorer

Theorem isch2

Description: Closed subspace H of a Hilbert space. Definition of Beran p. 107. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion isch2 ⊢H∈Cℋ↔H∈Sℋ∧∀f∀xf:ℕ⟶H∧f⇝vx→x∈H

Proof

Step Hyp Ref Expression
1 isch ⊢H∈Cℋ↔H∈Sℋ∧⇝vHℕ⊆H
2 alcom ⊢∀f∀xf∈Hℕ∧f⇝vx→x∈H↔∀x∀ff∈Hℕ∧f⇝vx→x∈H
3 19.23v ⊢∀ff∈Hℕ∧f⇝vx→x∈H↔∃ff∈Hℕ∧f⇝vx→x∈H
4 vex ⊢x∈V
5 4 elima2 ⊢x∈⇝vHℕ↔∃ff∈Hℕ∧f⇝vx
6 5 imbi1i ⊢x∈⇝vHℕ→x∈H↔∃ff∈Hℕ∧f⇝vx→x∈H
7 3 6 bitr4i ⊢∀ff∈Hℕ∧f⇝vx→x∈H↔x∈⇝vHℕ→x∈H
8 7 albii ⊢∀x∀ff∈Hℕ∧f⇝vx→x∈H↔∀xx∈⇝vHℕ→x∈H
9 dfss2 ⊢⇝vHℕ⊆H↔∀xx∈⇝vHℕ→x∈H
10 8 9 bitr4i ⊢∀x∀ff∈Hℕ∧f⇝vx→x∈H↔⇝vHℕ⊆H
11 2 10 bitri ⊢∀f∀xf∈Hℕ∧f⇝vx→x∈H↔⇝vHℕ⊆H
12 nnex ⊢ℕ∈V
13 elmapg ⊢H∈Sℋ∧ℕ∈V→f∈Hℕ↔f:ℕ⟶H
14 12 13 mpan2 ⊢H∈Sℋ→f∈Hℕ↔f:ℕ⟶H
15 14 anbi1d ⊢H∈Sℋ→f∈Hℕ∧f⇝vx↔f:ℕ⟶H∧f⇝vx
16 15 imbi1d ⊢H∈Sℋ→f∈Hℕ∧f⇝vx→x∈H↔f:ℕ⟶H∧f⇝vx→x∈H
17 16 2albidv ⊢H∈Sℋ→∀f∀xf∈Hℕ∧f⇝vx→x∈H↔∀f∀xf:ℕ⟶H∧f⇝vx→x∈H
18 11 17 bitr3id ⊢H∈Sℋ→⇝vHℕ⊆H↔∀f∀xf:ℕ⟶H∧f⇝vx→x∈H
19 18 pm5.32i ⊢H∈Sℋ∧⇝vHℕ⊆H↔H∈Sℋ∧∀f∀xf:ℕ⟶H∧f⇝vx→x∈H
20 1 19 bitri ⊢H∈Cℋ↔H∈Sℋ∧∀f∀xf:ℕ⟶H∧f⇝vx→x∈H