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 ⊢ ⊥ ⁡ ∅ = ℋ

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ y ∈ ∅ x ⋅ ih y = 0
2 0ss ⊢ ∅ ⊆ ℋ
3 ocel ⊢ ∅ ⊆ ℋ → x ∈ ⊥ ⁡ ∅ ↔ x ∈ ℋ ∧ ∀ y ∈ ∅ x ⋅ ih y = 0
4 2 3 ax-mp ⊢ x ∈ ⊥ ⁡ ∅ ↔ x ∈ ℋ ∧ ∀ y ∈ ∅ x ⋅ ih y = 0
5 1 4 mpbiran2 ⊢ x ∈ ⊥ ⁡ ∅ ↔ x ∈ ℋ
6 5 eqriv ⊢ ⊥ ⁡ ∅ = ℋ