Theorem bj-1upln0

Description: A monuple is nonempty. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-1upln0	$$⊢⦅A⦆\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-1upl	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA$$
2		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
3	2	necomi	$$⊢\left\{\varnothing \right\}\ne \varnothing$$
4		bj-tagn0	$$⊢tagA\ne \varnothing$$
5		xpnz	$$⊢\left(\left\{\varnothing \right\}\ne \varnothing \wedge tagA\ne \varnothing \right)\leftrightarrow \left\{\varnothing \right\}\times tagA\ne \varnothing$$
6	5	biimpi	$$⊢\left(\left\{\varnothing \right\}\ne \varnothing \wedge tagA\ne \varnothing \right)\to \left\{\varnothing \right\}\times tagA\ne \varnothing$$
7	3 4 6	mp2an	$$⊢\left\{\varnothing \right\}\times tagA\ne \varnothing$$
8	1 7	eqnetri	$$⊢⦅A⦆\ne \varnothing$$