Theorem bj-2upln0

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

	Ref	Expression
Assertion	bj-2upln0	|- (| A ,, B |) =/= (/)

Proof

Step	Hyp	Ref	Expression
1		df-bj-2upl	|- (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) )
2		bj-1upln0	|- (| A |) =/= (/)
3		0pss	|- ( (/) C. (| A |) <-> (| A |) =/= (/) )
4	2 3	mpbir	|- (/) C. (| A |)
5		ssun1	|- (| A |) C_ ( (| A |) u. ( { 1o } X. tag B ) )
6		psssstr	|- ( ( (/) C. (| A |) /\ (| A |) C_ ( (| A |) u. ( { 1o } X. tag B ) ) ) -> (/) C. ( (| A |) u. ( { 1o } X. tag B ) ) )
7	4 5 6	mp2an	|- (/) C. ( (| A |) u. ( { 1o } X. tag B ) )
8		0pss	|- ( (/) C. ( (| A |) u. ( { 1o } X. tag B ) ) <-> ( (| A |) u. ( { 1o } X. tag B ) ) =/= (/) )
9	7 8	mpbi	|- ( (| A |) u. ( { 1o } X. tag B ) ) =/= (/)
10	1 9	eqnetri	|- (| A ,, B |) =/= (/)