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

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 ∈ 𝒫 ℋ | ⊥ ⁡ ⊥ ⁡ x = x

Proof

Step Hyp Ref Expression
1 chss ⊢ x ∈ C ℋ → x ⊆ ℋ
2 ococ ⊢ x ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ x = x
3 1 2 jca ⊢ x ∈ C ℋ → x ⊆ ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
4 occl ⊢ x ⊆ ℋ → ⊥ ⁡ x ∈ C ℋ
5 chss ⊢ ⊥ ⁡ x ∈ C ℋ → ⊥ ⁡ x ⊆ ℋ
6 occl ⊢ ⊥ ⁡ x ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ x ∈ C ℋ
7 4 5 6 3syl ⊢ x ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ x ∈ C ℋ
8 eleq1 ⊢ ⊥ ⁡ ⊥ ⁡ x = x → ⊥ ⁡ ⊥ ⁡ x ∈ C ℋ ↔ x ∈ C ℋ
9 7 8 imbitrid ⊢ ⊥ ⁡ ⊥ ⁡ x = x → x ⊆ ℋ → x ∈ C ℋ
10 9 impcom ⊢ x ⊆ ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x → x ∈ C ℋ
11 3 10 impbii ⊢ x ∈ C ℋ ↔ x ⊆ ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
12 velpw ⊢ x ∈ 𝒫 ℋ ↔ x ⊆ ℋ
13 12 anbi1i ⊢ x ∈ 𝒫 ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x ↔ x ⊆ ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
14 11 13 bitr4i ⊢ x ∈ C ℋ ↔ x ∈ 𝒫 ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
15 14 eqabi ⊢ C ℋ = x | x ∈ 𝒫 ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
16 df-rab ⊢ x ∈ 𝒫 ℋ | ⊥ ⁡ ⊥ ⁡ x = x = x | x ∈ 𝒫 ℋ ∧ ⊥ ⁡ ⊥ ⁡ x = x
17 15 16 eqtr4i ⊢ C ℋ = x ∈ 𝒫 ℋ | ⊥ ⁡ ⊥ ⁡ x = x