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 }