Theorem bj-2upln0

Description: A couple is nonempty. (Contributed by BJ, 21-Apr-2019)

	Ref	Expression
Assertion	bj-2upln0	$$⊢⦅A,B⦆\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
2		bj-1upln0	$$⊢⦅A⦆\ne \varnothing$$
3		0pss	$$⊢\varnothing \subset ⦅A⦆\leftrightarrow ⦅A⦆\ne \varnothing$$
4	2 3	mpbir	$$⊢\varnothing \subset ⦅A⦆$$
5		ssun1	$$⊢⦅A⦆\subseteq ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
6		psssstr	$$⊢\left(\varnothing \subset ⦅A⦆\wedge ⦅A⦆\subseteq ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)\to \varnothing \subset ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
7	4 5 6	mp2an	$$⊢\varnothing \subset ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
8		0pss	$$⊢\varnothing \subset ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\leftrightarrow ⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\ne \varnothing$$
9	7 8	mpbi	$$⊢⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\ne \varnothing$$
10	1 9	eqnetri	$$⊢⦅A,B⦆\ne \varnothing$$