Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-2upln1upl Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 xpundi 5417 . . . . . . 7 ({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))
21difeq2i 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 𝐵)) = ∅)
64, 5ax-mp 5 . . . . . . . . 9 (({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅
73, 6eqtr3i 2804 . . . . . . . 8 (({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅
8 disjdif2 4271 . . . . . . . 8 ((({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ → (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵))
97, 8ax-mp 5 . . . . . . 7 (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵)
10 1oex 7851 . . . . . . . . . 10 1o ∈ V
1110snnz 4542 . . . . . . . . 9 {1o} ≠ ∅
12 bj-tagn0 33539 . . . . . . . . 9 tag 𝐵 ≠ ∅
1311, 12pm3.2i 464 . . . . . . . 8 ({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅)
14 xpnz 5807 . . . . . . . 8 (({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1o} × tag 𝐵) ≠ ∅)
1513, 14mpbi 222 . . . . . . 7 ({1o} × tag 𝐵) ≠ ∅
169, 15eqnetri 3039 . . . . . 6 (({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅
172, 16eqnetrri 3040 . . . . 5 (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅
18 0pss 4239 . . . . 5 (∅ ⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ↔ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ≠ ∅)
1917, 18mpbir 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 𝐶)))
2220, 21ax-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 𝐶)))
2523, 24ax-mp 5 . . . . . . 7 (({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
2622, 25sstri 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 𝐴)
2928uneq1i 3986 . . . . . . . 8 (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵))
3027, 29eqtri 2802 . . . . . . 7 𝐴, 𝐵⦆ = (({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵))
3130difeq1i 3947 . . . . . 6 (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) = ((({∅} × tag 𝐴) ∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))
3226, 31sseqtr4i 3857 . . . . 5 (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
33 df-bj-1upl 33558 . . . . . 6 𝐶⦆ = ({∅} × tag 𝐶)
3433difeq2i 3948 . . . . 5 (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶))
3532, 34sseqtr4i 3857 . . . 4 (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
36 psssstr 3935 . . . 4 ((∅ ⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ∧ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag 𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆))
3719, 35, 36mp2an 682 . . 3 ∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)
38 0pss 4239 . . 3 (∅ ⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅)
3937, 38mpbi 222 . 2 (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅
40 difn0 4173 . 2 ((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ → ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆)
4139, 40ax-mp 5 1 𝐴, 𝐵⦆ ≠ ⦅𝐶
Colors of variables: wff setvar class
Syntax hints:  wa 386   = wceq 1601  wne 2969  cdif 3789  cun 3790  cin 3791  wss 3792  wpss 3793  c0 4141  {csn 4398   × cxp 5353  1oc1o 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)
  Copyright terms: Public domain W3C validator