Theorem bj-1upln0

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

	Ref	Expression
Assertion	bj-1upln0	⊢ ⦅ 𝐴 ⦆ ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		df-bj-1upl	⊢ ⦅ 𝐴 ⦆ = ( { ∅ } × tag 𝐴 )
2		0nep0	⊢ ∅ ≠ { ∅ }
3	2	necomi	⊢ { ∅ } ≠ ∅
4		bj-tagn0	⊢ tag 𝐴 ≠ ∅
5		xpnz	⊢ ( ( { ∅ } ≠ ∅ ∧ tag 𝐴 ≠ ∅ ) ↔ ( { ∅ } × tag 𝐴 ) ≠ ∅ )
6	5	biimpi	⊢ ( ( { ∅ } ≠ ∅ ∧ tag 𝐴 ≠ ∅ ) → ( { ∅ } × tag 𝐴 ) ≠ ∅ )
7	3 4 6	mp2an	⊢ ( { ∅ } × tag 𝐴 ) ≠ ∅
8	1 7	eqnetri	⊢ ⦅ 𝐴 ⦆ ≠ ∅