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 ${⊢}{\mathbf{C}}_{ℋ}=\left\{{x}\in 𝒫ℋ|\perp \left(\perp \left({x}\right)\right)={x}\right\}$

Proof

Step Hyp Ref Expression
1 chss ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {x}\subseteq ℋ$
2 ococ ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({x}\right)\right)={x}$
3 1 2 jca ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({x}\subseteq ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)$
4 occl ${⊢}{x}\subseteq ℋ\to \perp \left({x}\right)\in {\mathbf{C}}_{ℋ}$
5 chss ${⊢}\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \perp \left({x}\right)\subseteq ℋ$
6 occl ${⊢}\perp \left({x}\right)\subseteq ℋ\to \perp \left(\perp \left({x}\right)\right)\in {\mathbf{C}}_{ℋ}$
7 4 5 6 3syl ${⊢}{x}\subseteq ℋ\to \perp \left(\perp \left({x}\right)\right)\in {\mathbf{C}}_{ℋ}$
8 eleq1 ${⊢}\perp \left(\perp \left({x}\right)\right)={x}\to \left(\perp \left(\perp \left({x}\right)\right)\in {\mathbf{C}}_{ℋ}↔{x}\in {\mathbf{C}}_{ℋ}\right)$
9 7 8 syl5ib ${⊢}\perp \left(\perp \left({x}\right)\right)={x}\to \left({x}\subseteq ℋ\to {x}\in {\mathbf{C}}_{ℋ}\right)$
10 9 impcom ${⊢}\left({x}\subseteq ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)\to {x}\in {\mathbf{C}}_{ℋ}$
11 3 10 impbii ${⊢}{x}\in {\mathbf{C}}_{ℋ}↔\left({x}\subseteq ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)$
12 velpw ${⊢}{x}\in 𝒫ℋ↔{x}\subseteq ℋ$
13 12 anbi1i ${⊢}\left({x}\in 𝒫ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)↔\left({x}\subseteq ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)$
14 11 13 bitr4i ${⊢}{x}\in {\mathbf{C}}_{ℋ}↔\left({x}\in 𝒫ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)$
15 14 abbi2i ${⊢}{\mathbf{C}}_{ℋ}=\left\{{x}|\left({x}\in 𝒫ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)\right\}$
16 df-rab ${⊢}\left\{{x}\in 𝒫ℋ|\perp \left(\perp \left({x}\right)\right)={x}\right\}=\left\{{x}|\left({x}\in 𝒫ℋ\wedge \perp \left(\perp \left({x}\right)\right)={x}\right)\right\}$
17 15 16 eqtr4i ${⊢}{\mathbf{C}}_{ℋ}=\left\{{x}\in 𝒫ℋ|\perp \left(\perp \left({x}\right)\right)={x}\right\}$