chocnul

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

		Ref	Expression
	Assertion	chocnul	$⊢ ⊥ (\emptyset) = ℋ$

Step	Hyp	Ref	Expression
1		ral0	$⊢ \forall y \in \emptyset x \cdot_{ih} y = 0$
2		0ss	$⊢ \emptyset \subseteq ℋ$
3		ocel	$⊢ \emptyset \subseteq ℋ \to (x \in ⊥ (\emptyset) \leftrightarrow (x \in ℋ \land \forall y \in \emptyset x \cdot_{ih} y = 0))$
4	2 3	ax-mp	$⊢ x \in ⊥ (\emptyset) \leftrightarrow (x \in ℋ \land \forall y \in \emptyset x \cdot_{ih} y = 0)$
5	1 4	mpbiran2	$⊢ x \in ⊥ (\emptyset) \leftrightarrow x \in ℋ$
6	5	eqriv	$⊢ ⊥ (\emptyset) = ℋ$

Metamath Proof Explorer