# 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 C_ ~H -> ( _|_ ` A ) e. CH )`

### Proof

Step Hyp Ref Expression
1 ocsh
` |-  ( A C_ ~H -> ( _|_ ` A ) e. SH )`
2 ax-hcompl
` |-  ( f e. Cauchy -> E. x e. ~H f ~~>v x )`
3 vex
` |-  f e. _V`
4 vex
` |-  x e. _V`
5 3 4 breldm
` |-  ( f ~~>v x -> f e. dom ~~>v )`
6 5 rexlimivw
` |-  ( E. x e. ~H f ~~>v x -> f e. dom ~~>v )`
7 2 6 syl
` |-  ( f e. Cauchy -> f e. dom ~~>v )`
8 7 ad2antlr
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> f e. dom ~~>v )`
9 hlimf
` |-  ~~>v : dom ~~>v --> ~H`
10 9 ffvelrni
` |-  ( f e. dom ~~>v -> ( ~~>v ` f ) e. ~H )`
11 8 10 syl
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> ( ~~>v ` f ) e. ~H )`
12 simplll
` |-  ( ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) /\ x e. A ) -> A C_ ~H )`
13 simpllr
` |-  ( ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) /\ x e. A ) -> f e. Cauchy )`
14 simplr
` |-  ( ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) /\ x e. A ) -> f : NN --> ( _|_ ` A ) )`
15 simpr
` |-  ( ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) /\ x e. A ) -> x e. A )`
16 12 13 14 15 occllem
` |-  ( ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) /\ x e. A ) -> ( ( ~~>v ` f ) .ih x ) = 0 )`
17 16 ralrimiva
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> A. x e. A ( ( ~~>v ` f ) .ih x ) = 0 )`
18 ocel
` |-  ( A C_ ~H -> ( ( ~~>v ` f ) e. ( _|_ ` A ) <-> ( ( ~~>v ` f ) e. ~H /\ A. x e. A ( ( ~~>v ` f ) .ih x ) = 0 ) ) )`
19 18 ad2antrr
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> ( ( ~~>v ` f ) e. ( _|_ ` A ) <-> ( ( ~~>v ` f ) e. ~H /\ A. x e. A ( ( ~~>v ` f ) .ih x ) = 0 ) ) )`
20 11 17 19 mpbir2and
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> ( ~~>v ` f ) e. ( _|_ ` A ) )`
21 ffun
` |-  ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v )`
22 funfvbrb
` |-  ( Fun ~~>v -> ( f e. dom ~~>v <-> f ~~>v ( ~~>v ` f ) ) )`
23 9 21 22 mp2b
` |-  ( f e. dom ~~>v <-> f ~~>v ( ~~>v ` f ) )`
24 8 23 sylib
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> f ~~>v ( ~~>v ` f ) )`
25 breq2
` |-  ( x = ( ~~>v ` f ) -> ( f ~~>v x <-> f ~~>v ( ~~>v ` f ) ) )`
26 25 rspcev
` |-  ( ( ( ~~>v ` f ) e. ( _|_ ` A ) /\ f ~~>v ( ~~>v ` f ) ) -> E. x e. ( _|_ ` A ) f ~~>v x )`
27 20 24 26 syl2anc
` |-  ( ( ( A C_ ~H /\ f e. Cauchy ) /\ f : NN --> ( _|_ ` A ) ) -> E. x e. ( _|_ ` A ) f ~~>v x )`
28 27 ex
` |-  ( ( A C_ ~H /\ f e. Cauchy ) -> ( f : NN --> ( _|_ ` A ) -> E. x e. ( _|_ ` A ) f ~~>v x ) )`
29 28 ralrimiva
` |-  ( A C_ ~H -> A. f e. Cauchy ( f : NN --> ( _|_ ` A ) -> E. x e. ( _|_ ` A ) f ~~>v x ) )`
30 isch3
` |-  ( ( _|_ ` A ) e. CH <-> ( ( _|_ ` A ) e. SH /\ A. f e. Cauchy ( f : NN --> ( _|_ ` A ) -> E. x e. ( _|_ ` A ) f ~~>v x ) ) )`
31 1 29 30 sylanbrc
` |-  ( A C_ ~H -> ( _|_ ` A ) e. CH )`