Metamath Proof Explorer

Theorem dfch2

Description: Alternate definition of the Hilbert lattice. (Contributed by NM, 8-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfch2	$⊢ C_{ℋ} = \{x \in 𝒫 ℋ \| ⊥ (⊥ (x)) = x\}$

Proof

Step	Hyp	Ref	Expression
1		chss	$⊢ x \in C_{ℋ} \to x \subseteq ℋ$
2		ococ	$⊢ x \in C_{ℋ} \to ⊥ (⊥ (x)) = x$
3	1 2	jca	$⊢ x \in C_{ℋ} \to (x \subseteq ℋ \land ⊥ (⊥ (x)) = x)$
4		occl	$⊢ x \subseteq ℋ \to ⊥ (x) \in C_{ℋ}$
5		chss	$⊢ ⊥ (x) \in C_{ℋ} \to ⊥ (x) \subseteq ℋ$
6		occl	$⊢ ⊥ (x) \subseteq ℋ \to ⊥ (⊥ (x)) \in C_{ℋ}$
7	4 5 6	3syl	$⊢ x \subseteq ℋ \to ⊥ (⊥ (x)) \in C_{ℋ}$
8		eleq1	$⊢ ⊥ (⊥ (x)) = x \to (⊥ (⊥ (x)) \in C_{ℋ} \leftrightarrow x \in C_{ℋ})$
9	7 8	imbitrid	$⊢ ⊥ (⊥ (x)) = x \to (x \subseteq ℋ \to x \in C_{ℋ})$
10	9	impcom	$⊢ (x \subseteq ℋ \land ⊥ (⊥ (x)) = x) \to x \in C_{ℋ}$
11	3 10	impbii	$⊢ x \in C_{ℋ} \leftrightarrow (x \subseteq ℋ \land ⊥ (⊥ (x)) = x)$
12		velpw	$⊢ x \in 𝒫 ℋ \leftrightarrow x \subseteq ℋ$
13	12	anbi1i	$⊢ (x \in 𝒫 ℋ \land ⊥ (⊥ (x)) = x) \leftrightarrow (x \subseteq ℋ \land ⊥ (⊥ (x)) = x)$
14	11 13	bitr4i	$⊢ x \in C_{ℋ} \leftrightarrow (x \in 𝒫 ℋ \land ⊥ (⊥ (x)) = x)$
15	14	eqabi	$⊢ C_{ℋ} = \{x \| (x \in 𝒫 ℋ \land ⊥ (⊥ (x)) = x)\}$
16		df-rab	$⊢ \{x \in 𝒫 ℋ \| ⊥ (⊥ (x)) = x\} = \{x \| (x \in 𝒫 ℋ \land ⊥ (⊥ (x)) = x)\}$
17	15 16	eqtr4i	$⊢ C_{ℋ} = \{x \in 𝒫 ℋ \| ⊥ (⊥ (x)) = x\}$