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	⊢ ∀ 𝑦 ∈ ∅ ( 𝑥 ·ih 𝑦 ) = 0
2		0ss	⊢ ∅ ⊆ ℋ
3		ocel	⊢ ( ∅ ⊆ ℋ → ( 𝑥 ∈ ( ⊥ ‘ ∅ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ∅ ( 𝑥 ·ih 𝑦 ) = 0 ) ) )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ ( ⊥ ‘ ∅ ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑦 ∈ ∅ ( 𝑥 ·ih 𝑦 ) = 0 ) )
5	1 4	mpbiran2	⊢ ( 𝑥 ∈ ( ⊥ ‘ ∅ ) ↔ 𝑥 ∈ ℋ )
6	5	eqriv	⊢ ( ⊥ ‘ ∅ ) = ℋ