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 } |