Description: Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | chocnul | |- ( _|_ ` (/) ) = ~H |
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 |