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 ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 isch ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) )
2 alcom ⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
3 19.23v ⊢ ( ∀ 𝑓 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ∃ 𝑓 ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
4 vex ⊢ 𝑥 ∈ V
5 4 elima2 ⊢ ( 𝑥 ∈ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) )
6 5 imbi1i ⊢ ( ( 𝑥 ∈ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) → 𝑥 ∈ 𝐻 ) ↔ ( ∃ 𝑓 ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
7 3 6 bitr4i ⊢ ( ∀ 𝑓 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( 𝑥 ∈ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) → 𝑥 ∈ 𝐻 ) )
8 7 albii ⊢ ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) → 𝑥 ∈ 𝐻 ) )
9 df-ss ⊢ ( ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) → 𝑥 ∈ 𝐻 ) )
10 8 9 bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 )
11 2 10 bitri ⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 )
12 nnex ⊢ ℕ ∈ V
13 elmapg ⊢ ( ( 𝐻 ∈ Sℋ ∧ ℕ ∈ V ) → ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐻 ) )
14 12 13 mpan2 ⊢ ( 𝐻 ∈ Sℋ → ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝐻 ) )
15 14 anbi1d ⊢ ( 𝐻 ∈ Sℋ → ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) ↔ ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) )
16 15 imbi1d ⊢ ( 𝐻 ∈ Sℋ → ( ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
17 16 2albidv ⊢ ( 𝐻 ∈ Sℋ → ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 ∈ ( 𝐻 ↑m ℕ ) ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
18 11 17 bitr3id ⊢ ( 𝐻 ∈ Sℋ → ( ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ↔ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
19 18 pm5.32i ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
20 1 19 bitri ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )