Metamath Proof Explorer


Theorem chocnul

Description: Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000) (New usage is discouraged.)

Ref Expression
Assertion chocnul
|- ( _|_ ` (/) ) = ~H

Proof

Step Hyp Ref Expression
1 ral0
 |-  A. y e. (/) ( x .ih y ) = 0
2 0ss
 |-  (/) C_ ~H
3 ocel
 |-  ( (/) C_ ~H -> ( x e. ( _|_ ` (/) ) <-> ( x e. ~H /\ A. y e. (/) ( x .ih y ) = 0 ) ) )
4 2 3 ax-mp
 |-  ( x e. ( _|_ ` (/) ) <-> ( x e. ~H /\ A. y e. (/) ( x .ih y ) = 0 ) )
5 1 4 mpbiran2
 |-  ( x e. ( _|_ ` (/) ) <-> x e. ~H )
6 5 eqriv
 |-  ( _|_ ` (/) ) = ~H