Step |
Hyp |
Ref |
Expression |
1 |
|
h1did |
|- ( A e. ~H -> A e. ( _|_ ` ( _|_ ` { A } ) ) ) |
2 |
|
eleq2 |
|- ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> ( A e. ( _|_ ` ( _|_ ` { A } ) ) <-> A e. 0H ) ) |
3 |
1 2
|
syl5ibcom |
|- ( A e. ~H -> ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> A e. 0H ) ) |
4 |
|
elch0 |
|- ( A e. 0H <-> A = 0h ) |
5 |
3 4
|
syl6ib |
|- ( A e. ~H -> ( ( _|_ ` ( _|_ ` { A } ) ) = 0H -> A = 0h ) ) |
6 |
5
|
necon3d |
|- ( A e. ~H -> ( A =/= 0h -> ( _|_ ` ( _|_ ` { A } ) ) =/= 0H ) ) |
7 |
6
|
imp |
|- ( ( A e. ~H /\ A =/= 0h ) -> ( _|_ ` ( _|_ ` { A } ) ) =/= 0H ) |