Metamath Proof Explorer

Theorem ococin

Description: The double complement is the smallest closed subspace containing a subset of Hilbert space. Remark 3.12(B) of Beran p. 107. (Contributed by NM, 8-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ococin 
|- ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) = |^| { x e. CH | A C_ x } )

Proof

Step Hyp Ref Expression
1 helch 
 |-  ~H e. CH
2 1 jctl 
 |-  ( A C_ ~H -> ( ~H e. CH /\ A C_ ~H ) )
3 sseq2 
 |-  ( x = ~H -> ( A C_ x <-> A C_ ~H ) )
4 3 elrab 
 |-  ( ~H e. { x e. CH | A C_ x } <-> ( ~H e. CH /\ A C_ ~H ) )
5 2 4 sylibr 
 |-  ( A C_ ~H -> ~H e. { x e. CH | A C_ x } )
6 intss1 
 |-  ( ~H e. { x e. CH | A C_ x } -> |^| { x e. CH | A C_ x } C_ ~H )
7 5 6 syl 
 |-  ( A C_ ~H -> |^| { x e. CH | A C_ x } C_ ~H )
8 ocss 
 |-  ( |^| { x e. CH | A C_ x } C_ ~H -> ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ~H )
9 7 8 syl 
 |-  ( A C_ ~H -> ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ~H )
10 ocss 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
11 9 10 jca 
 |-  ( A C_ ~H -> ( ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ~H /\ ( _|_ ` A ) C_ ~H ) )
12 ssintub 
 |-  A C_ |^| { x e. CH | A C_ x }
13 occon 
 |-  ( ( A C_ ~H /\ |^| { x e. CH | A C_ x } C_ ~H ) -> ( A C_ |^| { x e. CH | A C_ x } -> ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ( _|_ ` A ) ) )
14 7 13 mpdan 
 |-  ( A C_ ~H -> ( A C_ |^| { x e. CH | A C_ x } -> ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ( _|_ ` A ) ) )
15 12 14 mpi 
 |-  ( A C_ ~H -> ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ( _|_ ` A ) )
16 occon 
 |-  ( ( ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( ( _|_ ` |^| { x e. CH | A C_ x } ) C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` |^| { x e. CH | A C_ x } ) ) ) )
17 11 15 16 sylc 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` |^| { x e. CH | A C_ x } ) ) )
18 ssrab2 
 |-  { x e. CH | A C_ x } C_ CH
19 3 rspcev 
 |-  ( ( ~H e. CH /\ A C_ ~H ) -> E. x e. CH A C_ x )
20 1 19 mpan 
 |-  ( A C_ ~H -> E. x e. CH A C_ x )
21 rabn0 
 |-  ( { x e. CH | A C_ x } =/= (/) <-> E. x e. CH A C_ x )
22 20 21 sylibr 
 |-  ( A C_ ~H -> { x e. CH | A C_ x } =/= (/) )
23 chintcl 
 |-  ( ( { x e. CH | A C_ x } C_ CH /\ { x e. CH | A C_ x } =/= (/) ) -> |^| { x e. CH | A C_ x } e. CH )
24 18 22 23 sylancr 
 |-  ( A C_ ~H -> |^| { x e. CH | A C_ x } e. CH )
25 ococ 
 |-  ( |^| { x e. CH | A C_ x } e. CH -> ( _|_ ` ( _|_ ` |^| { x e. CH | A C_ x } ) ) = |^| { x e. CH | A C_ x } )
26 24 25 syl 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` |^| { x e. CH | A C_ x } ) ) = |^| { x e. CH | A C_ x } )
27 17 26 sseqtrd 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) C_ |^| { x e. CH | A C_ x } )
28 occl 
 |-  ( ( _|_ ` A ) C_ ~H -> ( _|_ ` ( _|_ ` A ) ) e. CH )
29 10 28 syl 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) e. CH )
30 ococss 
 |-  ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) )
31 sseq2 
 |-  ( x = ( _|_ ` ( _|_ ` A ) ) -> ( A C_ x <-> A C_ ( _|_ ` ( _|_ ` A ) ) ) )
32 31 elrab 
 |-  ( ( _|_ ` ( _|_ ` A ) ) e. { x e. CH | A C_ x } <-> ( ( _|_ ` ( _|_ ` A ) ) e. CH /\ A C_ ( _|_ ` ( _|_ ` A ) ) ) )
33 29 30 32 sylanbrc 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) e. { x e. CH | A C_ x } )
34 intss1 
 |-  ( ( _|_ ` ( _|_ ` A ) ) e. { x e. CH | A C_ x } -> |^| { x e. CH | A C_ x } C_ ( _|_ ` ( _|_ ` A ) ) )
35 33 34 syl 
 |-  ( A C_ ~H -> |^| { x e. CH | A C_ x } C_ ( _|_ ` ( _|_ ` A ) ) )
36 27 35 eqssd 
 |-  ( A C_ ~H -> ( _|_ ` ( _|_ ` A ) ) = |^| { x e. CH | A C_ x } )