Theorem bj-0nmoore

Description: The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-0nmoore	$$⊢\neg \varnothing \in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg \bigcup \varnothing \in \varnothing$$
2		bj-ismoored0	$$⊢\varnothing \in \underset{\_}{\mathrm{Moore}}\to \bigcup \varnothing \in \varnothing$$
3	1 2	mto	$$⊢\neg \varnothing \in \underset{\_}{\mathrm{Moore}}$$