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ℋ = { 𝑥 ∈ 𝒫 ℋ ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 }

Proof

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