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 \subseteq ℋ \to ⊥ (⊥ (A)) = ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$

Proof

Step	Hyp	Ref	Expression
1		helch	$⊢ ℋ \in C_{ℋ}$
2	1	jctl	$⊢ A \subseteq ℋ \to (ℋ \in C_{ℋ} \land A \subseteq ℋ)$
3		sseq2	$⊢ x = ℋ \to (A \subseteq x \leftrightarrow A \subseteq ℋ)$
4	3	elrab	$⊢ ℋ \in \{x \in C_{ℋ} \| A \subseteq x\} \leftrightarrow (ℋ \in C_{ℋ} \land A \subseteq ℋ)$
5	2 4	sylibr	$⊢ A \subseteq ℋ \to ℋ \in \{x \in C_{ℋ} \| A \subseteq x\}$
6		intss1	$⊢ ℋ \in \{x \in C_{ℋ} \| A \subseteq x\} \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ℋ$
7	5 6	syl	$⊢ A \subseteq ℋ \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ℋ$
8		ocss	$⊢ ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ℋ \to ⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ℋ$
9	7 8	syl	$⊢ A \subseteq ℋ \to ⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ℋ$
10		ocss	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
11	9 10	jca	$⊢ A \subseteq ℋ \to (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ℋ \land ⊥ (A) \subseteq ℋ)$
12		ssintub	$⊢ A \subseteq ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$
13		occon	$⊢ (A \subseteq ℋ \land ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ℋ) \to (A \subseteq ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \to ⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ⊥ (A))$
14	7 13	mpdan	$⊢ A \subseteq ℋ \to (A \subseteq ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \to ⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ⊥ (A))$
15	12 14	mpi	$⊢ A \subseteq ℋ \to ⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ⊥ (A)$
16		occon	$⊢ (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ℋ \land ⊥ (A) \subseteq ℋ) \to (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}) \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\})))$
17	11 15 16	sylc	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\}))$
18		ssrab2	$⊢ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq C_{ℋ}$
19	3	rspcev	$⊢ (ℋ \in C_{ℋ} \land A \subseteq ℋ) \to \exists x \in C_{ℋ} A \subseteq x$
20	1 19	mpan	$⊢ A \subseteq ℋ \to \exists x \in C_{ℋ} A \subseteq x$
21		rabn0	$⊢ \{x \in C_{ℋ} \| A \subseteq x\} \neq \emptyset \leftrightarrow \exists x \in C_{ℋ} A \subseteq x$
22	20 21	sylibr	$⊢ A \subseteq ℋ \to \{x \in C_{ℋ} \| A \subseteq x\} \neq \emptyset$
23		chintcl	$⊢ (\{x \in C_{ℋ} \| A \subseteq x\} \subseteq C_{ℋ} \land \{x \in C_{ℋ} \| A \subseteq x\} \neq \emptyset) \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \in C_{ℋ}$
24	18 22 23	sylancr	$⊢ A \subseteq ℋ \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \in C_{ℋ}$
25		ococ	$⊢ ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \in C_{ℋ} \to ⊥ (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\})) = ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$
26	24 25	syl	$⊢ A \subseteq ℋ \to ⊥ (⊥ (⋂ \{x \in C_{ℋ} \| A \subseteq x\})) = ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$
27	17 26	sseqtrd	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) \subseteq ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$
28		occl	$⊢ ⊥ (A) \subseteq ℋ \to ⊥ (⊥ (A)) \in C_{ℋ}$
29	10 28	syl	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) \in C_{ℋ}$
30		ococss	$⊢ A \subseteq ℋ \to A \subseteq ⊥ (⊥ (A))$
31		sseq2	$⊢ x = ⊥ (⊥ (A)) \to (A \subseteq x \leftrightarrow A \subseteq ⊥ (⊥ (A)))$
32	31	elrab	$⊢ ⊥ (⊥ (A)) \in \{x \in C_{ℋ} \| A \subseteq x\} \leftrightarrow (⊥ (⊥ (A)) \in C_{ℋ} \land A \subseteq ⊥ (⊥ (A)))$
33	29 30 32	sylanbrc	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) \in \{x \in C_{ℋ} \| A \subseteq x\}$
34		intss1	$⊢ ⊥ (⊥ (A)) \in \{x \in C_{ℋ} \| A \subseteq x\} \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ⊥ (⊥ (A))$
35	33 34	syl	$⊢ A \subseteq ℋ \to ⋂ \{x \in C_{ℋ} \| A \subseteq x\} \subseteq ⊥ (⊥ (A))$
36	27 35	eqssd	$⊢ A \subseteq ℋ \to ⊥ (⊥ (A)) = ⋂ \{x \in C_{ℋ} \| A \subseteq x\}$

Metamath Proof Explorer

Theorem ococin

Proof