Theorem bj-1upln0

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

	Ref	Expression
Assertion	bj-1upln0	|- (| A |) =/= (/)

Proof

Step	Hyp	Ref	Expression
1		df-bj-1upl	|- (| A |) = ( { (/) } X. tag A )
2		0nep0	|- (/) =/= { (/) }
3	2	necomi	|- { (/) } =/= (/)
4		bj-tagn0	|- tag A =/= (/)
5		xpnz	|- ( ( { (/) } =/= (/) /\ tag A =/= (/) ) <-> ( { (/) } X. tag A ) =/= (/) )
6	5	biimpi	|- ( ( { (/) } =/= (/) /\ tag A =/= (/) ) -> ( { (/) } X. tag A ) =/= (/) )
7	3 4 6	mp2an	|- ( { (/) } X. tag A ) =/= (/)
8	1 7	eqnetri	|- (| A |) =/= (/)