# Metamath Proof Explorer

## Theorem occl

Description: Closure of complement of Hilbert subset. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 8-Aug-2000) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion occl ${⊢}{A}\subseteq ℋ\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 ocsh ${⊢}{A}\subseteq ℋ\to \perp \left({A}\right)\in {\mathbf{S}}_{ℋ}$
2 ax-hcompl
3 vex ${⊢}{f}\in \mathrm{V}$
4 vex ${⊢}{x}\in \mathrm{V}$
5 3 4 breldm
6 5 rexlimivw
7 2 6 syl
9 hlimf
10 9 ffvelrni
11 8 10 syl
12 simplll ${⊢}\left(\left(\left({A}\subseteq ℋ\wedge {f}\in \mathrm{Cauchy}\right)\wedge {f}:ℕ⟶\perp \left({A}\right)\right)\wedge {x}\in {A}\right)\to {A}\subseteq ℋ$
13 simpllr ${⊢}\left(\left(\left({A}\subseteq ℋ\wedge {f}\in \mathrm{Cauchy}\right)\wedge {f}:ℕ⟶\perp \left({A}\right)\right)\wedge {x}\in {A}\right)\to {f}\in \mathrm{Cauchy}$
14 simplr ${⊢}\left(\left(\left({A}\subseteq ℋ\wedge {f}\in \mathrm{Cauchy}\right)\wedge {f}:ℕ⟶\perp \left({A}\right)\right)\wedge {x}\in {A}\right)\to {f}:ℕ⟶\perp \left({A}\right)$
15 simpr ${⊢}\left(\left(\left({A}\subseteq ℋ\wedge {f}\in \mathrm{Cauchy}\right)\wedge {f}:ℕ⟶\perp \left({A}\right)\right)\wedge {x}\in {A}\right)\to {x}\in {A}$
16 12 13 14 15 occllem
17 16 ralrimiva
18 ocel
31 1 29 30 sylanbrc ${⊢}{A}\subseteq ℋ\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$