Theorem bj-2upln1upl 32205

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 ⦅𝐴, ∅⦆ = ⦅𝐴⦆. 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 32190 and bj-2upln0 32204 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.)

Assertion

Ref	Expression
bj-2upln1upl	⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆

Proof of Theorem bj-2upln1upl

Step	Hyp	Ref	Expression
1		xpundi 5094	. . . . . . 7 ⊢ ({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
2	1	difeq2i 3687	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
3		incom 3767	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = (({1𝑜} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶)))
4		bj-disjsn01 32130	. . . . . . . . . 10 ⊢ ({∅} ∩ {1𝑜}) = ∅
5		xpdisj1 5474	. . . . . . . . . 10 ⊢ (({∅} ∩ {1𝑜}) = ∅ → (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = ∅)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = ∅
7	3, 6	eqtr3i 2634	. . . . . . . 8 ⊢ (({1𝑜} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅
8		disjdif2 3999	. . . . . . . 8 ⊢ ((({1𝑜} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ → (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1𝑜} × tag 𝐵))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1𝑜} × tag 𝐵)
10		bj-1ex 32131	. . . . . . . . . 10 ⊢ 1𝑜 ∈ V
11	10	snnz 4252	. . . . . . . . 9 ⊢ {1𝑜} ≠ ∅
12		bj-tagn0 32160	. . . . . . . . 9 ⊢ tag 𝐵 ≠ ∅
13	11, 12	pm3.2i 470	. . . . . . . 8 ⊢ ({1𝑜} ≠ ∅ ∧ tag 𝐵 ≠ ∅)
14		xpnz 5472	. . . . . . . 8 ⊢ (({1𝑜} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1𝑜} × tag 𝐵) ≠ ∅)
15	13, 14	mpbi 219	. . . . . . 7 ⊢ ({1𝑜} × tag 𝐵) ≠ ∅
16	9, 15	eqnetri 2852	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅
17	2, 16	eqnetrri 2853	. . . . 5 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅
18		0pss 3965	. . . . 5 ⊢ (∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ↔ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅)
19	17, 18	mpbir 220	. . . 4 ⊢ ∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
20		ssun2 3739	. . . . . . . 8 ⊢ ({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
21		sscon 3706	. . . . . . . 8 ⊢ (({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)) → (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (({1𝑜} × tag 𝐵) ∖ ({∅} × tag 𝐶)))
22	20, 21	ax-mp 5	. . . . . . 7 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (({1𝑜} × tag 𝐵) ∖ ({∅} × tag 𝐶))
23		ssun2 3739	. . . . . . . 8 ⊢ ({1𝑜} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
24		ssdif 3707	. . . . . . . 8 ⊢ (({1𝑜} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) → (({1𝑜} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶)))
25	23, 24	ax-mp 5	. . . . . . 7 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
26	22, 25	sstri 3577	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
27		df-bj-2upl 32192	. . . . . . . 8 ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))
28		df-bj-1upl 32179	. . . . . . . . 9 ⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
29	28	uneq1i 3725	. . . . . . . 8 ⊢ (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
30	27, 29	eqtri 2632	. . . . . . 7 ⊢ ⦅𝐴, 𝐵⦆ = (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
31	30	difeq1i 3686	. . . . . 6 ⊢ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) = ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
32	26, 31	sseqtr4i 3601	. . . . 5 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
33		df-bj-1upl 32179	. . . . . 6 ⊢ ⦅𝐶⦆ = ({∅} × tag 𝐶)
34	33	difeq2i 3687	. . . . 5 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
35	32, 34	sseqtr4i 3601	. . . 4 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
36		psssstr 3675	. . . 4 ⊢ ((∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ∧ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆))
37	19, 35, 36	mp2an 704	. . 3 ⊢ ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
38		0pss 3965	. . 3 ⊢ (∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅)
39	37, 38	mpbi 219	. 2 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅
40		difn0 3897	. 2 ⊢ ((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ → ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆)
41	39, 40	ax-mp 5	1 ⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆

Syntax hints:   ∧ wa 383   = wceq 1475   ≠ wne 2780   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540   ⊊ wpss 3541  ∅c0 3874  {csn 4125   × cxp 5036  1_𝑜c1o 7440  tag bj-ctag 32155  ⦅bj-c1upl 32178  ⦅bj-c2uple 32191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-suc 5646  df-1o 7447  df-bj-tag 32156  df-bj-1upl 32179  df-bj-2upl 32192

This theorem is referenced by: (None)