Theorem bj-2upln1upl

Description: A couple is never equal to a monuple. It is in order to have this "non-clashing" result that tagging was used. Without tagging, we would have (| A , (/) |) = (| A |) . Note that in the context of Morse tuples, it is natural to define the 0-tuple as the empty set. Therefore, the present theorem together with bj-1upln0 and bj-2upln0 tell us that an m-tuple may equal an n-tuple only when m = n, at least for m, n <= 2, but this result would extend as soon as we define n-tuples for higher values of n. (Contributed by BJ, 21-Apr-2019)

	Ref	Expression
Assertion	bj-2upln1upl	$$⊢⦅A,B⦆\ne ⦅C⦆$$

Proof

Step	Hyp	Ref	Expression
1		xpundi	$$⊢\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)=\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)$$
2	1	difeq2i	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)=\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)$$
3		incom	$$⊢\left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)\cap \left(\left\{1_{𝑜}\right\}\times tagB\right)=\left(\left\{1_{𝑜}\right\}\times tagB\right)\cap \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)$$
4		xp01disjl	$$⊢\left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)\cap \left(\left\{1_{𝑜}\right\}\times tagB\right)=\varnothing$$
5	3 4	eqtr3i	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\cap \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)=\varnothing$$
6		disjdif2	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\cap \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)=\varnothing \to \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)=\left\{1_{𝑜}\right\}\times tagB$$
7	5 6	ax-mp	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)=\left\{1_{𝑜}\right\}\times tagB$$
8		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
9	8	snnz	$$⊢\left\{1_{𝑜}\right\}\ne \varnothing$$
10		bj-tagn0	$$⊢tagB\ne \varnothing$$
11	9 10	pm3.2i	$$⊢\left(\left\{1_{𝑜}\right\}\ne \varnothing \wedge tagB\ne \varnothing \right)$$
12		xpnz	$$⊢\left(\left\{1_{𝑜}\right\}\ne \varnothing \wedge tagB\ne \varnothing \right)\leftrightarrow \left\{1_{𝑜}\right\}\times tagB\ne \varnothing$$
13	11 12	mpbi	$$⊢\left\{1_{𝑜}\right\}\times tagB\ne \varnothing$$
14	7 13	eqnetri	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times \left(tagA\cup tagC\right)\right)\ne \varnothing$$
15	2 14	eqnetrri	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\ne \varnothing$$
16		0pss	$$⊢\varnothing \subset \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\leftrightarrow \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\ne \varnothing$$
17	15 16	mpbir	$$⊢\varnothing \subset \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)$$
18		ssun2	$$⊢\left\{\varnothing \right\}\times tagC\subseteq \left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)$$
19		sscon	$$⊢\left\{\varnothing \right\}\times tagC\subseteq \left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\to \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
20	18 19	ax-mp	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
21		ssun2	$$⊢\left\{1_{𝑜}\right\}\times tagB\subseteq \left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
22		ssdif	$$⊢\left\{1_{𝑜}\right\}\times tagB\subseteq \left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\to \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)\subseteq \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
23	21 22	ax-mp	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)\subseteq \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
24	20 23	sstri	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
25		df-bj-2upl	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
26		df-bj-1upl	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA$$
27	26	uneq1i	$$⊢⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)=\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
28	25 27	eqtri	$$⊢⦅A,B⦆=\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$
29	28	difeq1i	$$⊢⦅A,B⦆\setminus \left(\left\{\varnothing \right\}\times tagC\right)=\left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
30	24 29	sseqtrri	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq ⦅A,B⦆\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
31		df-bj-1upl	$$⊢⦅C⦆=\left\{\varnothing \right\}\times tagC$$
32	31	difeq2i	$$⊢⦅A,B⦆\setminus ⦅C⦆=⦅A,B⦆\setminus \left(\left\{\varnothing \right\}\times tagC\right)$$
33	30 32	sseqtrri	$$⊢\left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq ⦅A,B⦆\setminus ⦅C⦆$$
34		psssstr	$$⊢\left(\varnothing \subset \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\wedge \left(\left\{1_{𝑜}\right\}\times tagB\right)\setminus \left(\left(\left\{\varnothing \right\}\times tagA\right)\cup \left(\left\{\varnothing \right\}\times tagC\right)\right)\subseteq ⦅A,B⦆\setminus ⦅C⦆\right)\to \varnothing \subset ⦅A,B⦆\setminus ⦅C⦆$$
35	17 33 34	mp2an	$$⊢\varnothing \subset ⦅A,B⦆\setminus ⦅C⦆$$
36		0pss	$$⊢\varnothing \subset ⦅A,B⦆\setminus ⦅C⦆\leftrightarrow ⦅A,B⦆\setminus ⦅C⦆\ne \varnothing$$
37	35 36	mpbi	$$⊢⦅A,B⦆\setminus ⦅C⦆\ne \varnothing$$
38		difn0	$$⊢⦅A,B⦆\setminus ⦅C⦆\ne \varnothing \to ⦅A,B⦆\ne ⦅C⦆$$
39	37 38	ax-mp	$$⊢⦅A,B⦆\ne ⦅C⦆$$