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 
|- 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 imbitrid 
 |-  ( ( _|_ ` ( _|_ ` 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 eqabi 
 |-  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 }