This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )

Proof

Step Hyp Ref Expression
1 helch ⊢ ℋ ∈ Cℋ
2 1 jctl ⊢ ( 𝐴 ⊆ ℋ → ( ℋ ∈ Cℋ ∧ 𝐴 ⊆ ℋ ) )
3 sseq2 ⊢ ( 𝑥 = ℋ → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ℋ ) )
4 3 elrab ⊢ ( ℋ ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ↔ ( ℋ ∈ Cℋ ∧ 𝐴 ⊆ ℋ ) )
5 2 4 sylibr ⊢ ( 𝐴 ⊆ ℋ → ℋ ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )
6 intss1 ⊢ ( ℋ ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ℋ )
7 5 6 syl ⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ℋ )
8 ocss ⊢ ( ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ℋ → ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ℋ )
9 7 8 syl ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ℋ )
10 ocss ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
11 9 10 jca ⊢ ( 𝐴 ⊆ ℋ → ( ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) )
12 ssintub ⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 }
13 occon ⊢ ( ( 𝐴 ⊆ ℋ ∧ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ℋ ) → ( 𝐴 ⊆ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } → ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
14 7 13 mpdan ⊢ ( 𝐴 ⊆ ℋ → ( 𝐴 ⊆ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } → ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
15 12 14 mpi ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ( ⊥ ‘ 𝐴 ) )
16 occon ⊢ ( ( ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) → ( ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ) ) )
17 11 15 16 sylc ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ) )
18 ssrab2 ⊢ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Cℋ
19 3 rspcev ⊢ ( ( ℋ ∈ Cℋ ∧ 𝐴 ⊆ ℋ ) → ∃ 𝑥 ∈ Cℋ 𝐴 ⊆ 𝑥 )
20 1 19 mpan ⊢ ( 𝐴 ⊆ ℋ → ∃ 𝑥 ∈ Cℋ 𝐴 ⊆ 𝑥 )
21 rabn0 ⊢ ( { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Cℋ 𝐴 ⊆ 𝑥 )
22 20 21 sylibr ⊢ ( 𝐴 ⊆ ℋ → { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ )
23 chintcl ⊢ ( ( { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Cℋ ∧ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Cℋ )
24 18 22 23 sylancr ⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Cℋ )
25 ococ ⊢ ( ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ) = ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )
26 24 25 syl ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ) ) = ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )
27 17 26 sseqtrd ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )
28 occl ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ )
29 10 28 syl ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ )
30 ococss ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
31 sseq2 ⊢ ( 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
32 31 elrab ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ↔ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
33 29 30 32 sylanbrc ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )
34 intss1 ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
35 33 34 syl ⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
36 27 35 eqssd ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = ∩ { 𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥 } )