Theorem bj-2upln1upl 33012

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 32997 and bj-2upln0 33011 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 5171	. . . . . . 7 ⊢ ({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
2	1	difeq2i 3725	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
3		incom 3805	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = (({1𝑜} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶)))
4		bj-disjsn01 32937	. . . . . . . . . 10 ⊢ ({∅} ∩ {1𝑜}) = ∅
5		xpdisj1 5555	. . . . . . . . . 10 ⊢ (({∅} ∩ {1𝑜}) = ∅ → (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = ∅)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1𝑜} × tag 𝐵)) = ∅
7	3, 6	eqtr3i 2646	. . . . . . . 8 ⊢ (({1𝑜} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅
8		disjdif2 4047	. . . . . . . 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 32938	. . . . . . . . . 10 ⊢ 1𝑜 ∈ V
11	10	snnz 4309	. . . . . . . . 9 ⊢ {1𝑜} ≠ ∅
12		bj-tagn0 32967	. . . . . . . . 9 ⊢ tag 𝐵 ≠ ∅
13	11, 12	pm3.2i 471	. . . . . . . 8 ⊢ ({1𝑜} ≠ ∅ ∧ tag 𝐵 ≠ ∅)
14		xpnz 5553	. . . . . . . 8 ⊢ (({1𝑜} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1𝑜} × tag 𝐵) ≠ ∅)
15	13, 14	mpbi 220	. . . . . . 7 ⊢ ({1𝑜} × tag 𝐵) ≠ ∅
16	9, 15	eqnetri 2864	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅
17	2, 16	eqnetrri 2865	. . . . 5 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅
18		0pss 4013	. . . . 5 ⊢ (∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ↔ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅)
19	17, 18	mpbir 221	. . . 4 ⊢ ∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
20		ssun2 3777	. . . . . . . 8 ⊢ ({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
21		sscon 3744	. . . . . . . 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 3777	. . . . . . . 8 ⊢ ({1𝑜} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
24		ssdif 3745	. . . . . . . 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 3612	. . . . . 6 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
27		df-bj-2upl 32999	. . . . . . . 8 ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))
28		df-bj-1upl 32986	. . . . . . . . 9 ⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
29	28	uneq1i 3763	. . . . . . . 8 ⊢ (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
30	27, 29	eqtri 2644	. . . . . . 7 ⊢ ⦅𝐴, 𝐵⦆ = (({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵))
31	30	difeq1i 3724	. . . . . 6 ⊢ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) = ((({∅} × tag 𝐴) ∪ ({1𝑜} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
32	26, 31	sseqtr4i 3638	. . . . 5 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
33		df-bj-1upl 32986	. . . . . 6 ⊢ ⦅𝐶⦆ = ({∅} × tag 𝐶)
34	33	difeq2i 3725	. . . . 5 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
35	32, 34	sseqtr4i 3638	. . . 4 ⊢ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
36		psssstr 3713	. . . 4 ⊢ ((∅ ⊊ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ∧ (({1𝑜} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆))
37	19, 35, 36	mp2an 708	. . 3 ⊢ ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
38		0pss 4013	. . 3 ⊢ (∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅)
39	37, 38	mpbi 220	. 2 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅
40		difn0 3943	. 2 ⊢ ((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ → ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆)
41	39, 40	ax-mp 5	1 ⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆

Syntax hints:   ∧ wa 384   = wceq 1483   ≠ wne 2794   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574   ⊊ wpss 3575  ∅c0 3915  {csn 4177   × cxp 5112  1_𝑜c1o 7553  tag bj-ctag 32962  ⦅bj-c1upl 32985  ⦅bj-c2uple 32998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-suc 5729  df-1o 7560  df-bj-tag 32963  df-bj-1upl 32986  df-bj-2upl 32999

This theorem is referenced by: (None)