Theorem bj-2upln1upl 33584

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 33569 and bj-2upln0 33583 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 5417	. . . . . . 7 ⊢ ({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
2	1	difeq2i 3948	. . . . . 6 ⊢ (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
3		incom 4028	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = (({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶)))
4		bj-disjsn01 33510	. . . . . . . . . 10 ⊢ ({∅} ∩ {1o}) = ∅
5		xpdisj1 5809	. . . . . . . . . 10 ⊢ (({∅} ∩ {1o}) = ∅ → (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅
7	3, 6	eqtr3i 2804	. . . . . . . 8 ⊢ (({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅
8		disjdif2 4271	. . . . . . . 8 ⊢ ((({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ → (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵)
10		1oex 7851	. . . . . . . . . 10 ⊢ 1o ∈ V
11	10	snnz 4542	. . . . . . . . 9 ⊢ {1o} ≠ ∅
12		bj-tagn0 33539	. . . . . . . . 9 ⊢ tag 𝐵 ≠ ∅
13	11, 12	pm3.2i 464	. . . . . . . 8 ⊢ ({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅)
14		xpnz 5807	. . . . . . . 8 ⊢ (({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1o} × tag 𝐵) ≠ ∅)
15	13, 14	mpbi 222	. . . . . . 7 ⊢ ({1o} × tag 𝐵) ≠ ∅
16	9, 15	eqnetri 3039	. . . . . 6 ⊢ (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅
17	2, 16	eqnetrri 3040	. . . . 5 ⊢ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅
18		0pss 4239	. . . . 5 ⊢ (∅ ⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ↔ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅)
19	17, 18	mpbir 223	. . . 4 ⊢ ∅ ⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)))
20		ssun2 4000	. . . . . . . 8 ⊢ ({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
21		sscon 3967	. . . . . . . 8 ⊢ (({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶)) → (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)))
22	20, 21	ax-mp 5	. . . . . . 7 ⊢ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶))
23		ssun2 4000	. . . . . . . 8 ⊢ ({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵))
24		ssdif 3968	. . . . . . . 8 ⊢ (({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) → (({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)))
25	23, 24	ax-mp 5	. . . . . . 7 ⊢ (({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
26	22, 25	sstri 3830	. . . . . 6 ⊢ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
27		df-bj-2upl 33571	. . . . . . . 8 ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
28		df-bj-1upl 33558	. . . . . . . . 9 ⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
29	28	uneq1i 3986	. . . . . . . 8 ⊢ (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵))
30	27, 29	eqtri 2802	. . . . . . 7 ⊢ ⦅𝐴, 𝐵⦆ = (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵))
31	30	difeq1i 3947	. . . . . 6 ⊢ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) = ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
32	26, 31	sseqtr4i 3857	. . . . 5 ⊢ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
33		df-bj-1upl 33558	. . . . . 6 ⊢ ⦅𝐶⦆ = ({∅} × tag 𝐶)
34	33	difeq2i 3948	. . . . 5 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
35	32, 34	sseqtr4i 3857	. . . 4 ⊢ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
36		psssstr 3935	. . . 4 ⊢ ((∅ ⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ∧ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆))
37	19, 35, 36	mp2an 682	. . 3 ⊢ ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
38		0pss 4239	. . 3 ⊢ (∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅)
39	37, 38	mpbi 222	. 2 ⊢ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅
40		difn0 4173	. 2 ⊢ ((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ → ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆)
41	39, 40	ax-mp 5	1 ⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆

Syntax hints:   ∧ wa 386   = wceq 1601   ≠ wne 2969   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792   ⊊ wpss 3793  ∅c0 4141  {csn 4398   × cxp 5353  1_oc1o 7836  tag bj-ctag 33534  ⦅bj-c1upl 33557  ⦅bj-c2uple 33570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-ord 5979  df-on 5980  df-suc 5982  df-1o 7843  df-bj-tag 33535  df-bj-1upl 33558  df-bj-2upl 33571

This theorem is referenced by: (None)