Step |
Hyp |
Ref |
Expression |
1 |
|
ococ.1 |
|- A e. CH |
2 |
1
|
chshii |
|- A e. SH |
3 |
|
shocsh |
|- ( A e. SH -> ( _|_ ` A ) e. SH ) |
4 |
2 3
|
ax-mp |
|- ( _|_ ` A ) e. SH |
5 |
|
shocsh |
|- ( ( _|_ ` A ) e. SH -> ( _|_ ` ( _|_ ` A ) ) e. SH ) |
6 |
4 5
|
ax-mp |
|- ( _|_ ` ( _|_ ` A ) ) e. SH |
7 |
|
shococss |
|- ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) ) |
8 |
2 7
|
ax-mp |
|- A C_ ( _|_ ` ( _|_ ` A ) ) |
9 |
|
incom |
|- ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) |
10 |
|
ocin |
|- ( ( _|_ ` A ) e. SH -> ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H ) |
11 |
4 10
|
ax-mp |
|- ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H |
12 |
9 11
|
eqtri |
|- ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = 0H |
13 |
1 6 8 12
|
omlsii |
|- A = ( _|_ ` ( _|_ ` A ) ) |
14 |
13
|
eqcomi |
|- ( _|_ ` ( _|_ ` A ) ) = A |