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
|- CH = { x e. ~P ~H | ( _|_ ` ( _|_ ` x ) ) = x }

Proof

Step Hyp Ref Expression
1 chss
 |-  ( x e. CH -> x C_ ~H )
2 ococ
 |-  ( x e. CH -> ( _|_ ` ( _|_ ` x ) ) = x )
3 1 2 jca
 |-  ( x e. CH -> ( x C_ ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) )
4 occl
 |-  ( x C_ ~H -> ( _|_ ` x ) e. CH )
5 chss
 |-  ( ( _|_ ` x ) e. CH -> ( _|_ ` x ) C_ ~H )
6 occl
 |-  ( ( _|_ ` x ) C_ ~H -> ( _|_ ` ( _|_ ` x ) ) e. CH )
7 4 5 6 3syl
 |-  ( x C_ ~H -> ( _|_ ` ( _|_ ` x ) ) e. CH )
8 eleq1
 |-  ( ( _|_ ` ( _|_ ` x ) ) = x -> ( ( _|_ ` ( _|_ ` x ) ) e. CH <-> x e. CH ) )
9 7 8 syl5ib
 |-  ( ( _|_ ` ( _|_ ` x ) ) = x -> ( x C_ ~H -> x e. CH ) )
10 9 impcom
 |-  ( ( x C_ ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) -> x e. CH )
11 3 10 impbii
 |-  ( x e. CH <-> ( x C_ ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) )
12 velpw
 |-  ( x e. ~P ~H <-> x C_ ~H )
13 12 anbi1i
 |-  ( ( x e. ~P ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) <-> ( x C_ ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) )
14 11 13 bitr4i
 |-  ( x e. CH <-> ( x e. ~P ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) )
15 14 abbi2i
 |-  CH = { x | ( x e. ~P ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) }
16 df-rab
 |-  { x e. ~P ~H | ( _|_ ` ( _|_ ` x ) ) = x } = { x | ( x e. ~P ~H /\ ( _|_ ` ( _|_ ` x ) ) = x ) }
17 15 16 eqtr4i
 |-  CH = { x e. ~P ~H | ( _|_ ` ( _|_ ` x ) ) = x }