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 ffvelcdmi 
 |-  ( 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 )