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ℋ ∣ 𝐴 ⊆ 𝑥 } )