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