Step |
Hyp |
Ref |
Expression |
1 |
|
ch0le.1 |
|- A e. CH |
2 |
|
chjcl.2 |
|- B e. CH |
3 |
1 2
|
chsscon2i |
|- ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) |
4 |
2 1
|
chsscon1i |
|- ( ( _|_ ` B ) C_ A <-> ( _|_ ` A ) C_ B ) |
5 |
3 4
|
anbi12i |
|- ( ( A C_ ( _|_ ` B ) /\ ( _|_ ` B ) C_ A ) <-> ( B C_ ( _|_ ` A ) /\ ( _|_ ` A ) C_ B ) ) |
6 |
|
eqss |
|- ( A = ( _|_ ` B ) <-> ( A C_ ( _|_ ` B ) /\ ( _|_ ` B ) C_ A ) ) |
7 |
|
eqss |
|- ( B = ( _|_ ` A ) <-> ( B C_ ( _|_ ` A ) /\ ( _|_ ` A ) C_ B ) ) |
8 |
5 6 7
|
3bitr4i |
|- ( A = ( _|_ ` B ) <-> B = ( _|_ ` A ) ) |