Metamath Proof Explorer

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 ⦅ 𝐴 , 𝐵 ⦆ ≠ ⦅ 𝐶 ⦆

Proof

Step Hyp Ref Expression
1 xpundi ⊢ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) = ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) )
2 1 difeq2i ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) = ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) )
3 incom ⊢ ( ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ∩ ( { 1o } × tag 𝐵 ) ) = ( ( { 1o } × tag 𝐵 ) ∩ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) )
4 xp01disjl ⊢ ( ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ∩ ( { 1o } × tag 𝐵 ) ) = ∅
5 3 4 eqtr3i ⊢ ( ( { 1o } × tag 𝐵 ) ∩ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) = ∅
6 disjdif2 ⊢ ( ( ( { 1o } × tag 𝐵 ) ∩ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) = ∅ → ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) = ( { 1o } × tag 𝐵 ) )
7 5 6 ax-mp ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) = ( { 1o } × tag 𝐵 )
8 1oex ⊢ 1o ∈ V
9 8 snnz ⊢ { 1o } ≠ ∅
10 bj-tagn0 ⊢ tag 𝐵 ≠ ∅
11 9 10 pm3.2i ⊢ ( { 1o } ≠ ∅ ∧ tag 𝐵 ≠ ∅ )
12 xpnz ⊢ ( ( { 1o } ≠ ∅ ∧ tag 𝐵 ≠ ∅ ) ↔ ( { 1o } × tag 𝐵 ) ≠ ∅ )
13 11 12 mpbi ⊢ ( { 1o } × tag 𝐵 ) ≠ ∅
14 7 13 eqnetri ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × ( tag 𝐴 ∪ tag 𝐶 ) ) ) ≠ ∅
15 2 14 eqnetrri ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ≠ ∅
16 0pss ⊢ ( ∅ ⊊ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ↔ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ≠ ∅ )
17 15 16 mpbir ⊢ ∅ ⊊ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) )
18 ssun2 ⊢ ( { ∅ } × tag 𝐶 ) ⊆ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) )
19 sscon ⊢ ( ( { ∅ } × tag 𝐶 ) ⊆ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) → ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × tag 𝐶 ) ) )
20 18 19 ax-mp ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × tag 𝐶 ) )
21 ssun2 ⊢ ( { 1o } × tag 𝐵 ) ⊆ ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) )
22 ssdif ⊢ ( ( { 1o } × tag 𝐵 ) ⊆ ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) ) → ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × tag 𝐶 ) ) ⊆ ( ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) ) ∖ ( { ∅ } × tag 𝐶 ) ) )
23 21 22 ax-mp ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( { ∅ } × tag 𝐶 ) ) ⊆ ( ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) ) ∖ ( { ∅ } × tag 𝐶 ) )
24 20 23 sstri ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) ) ∖ ( { ∅ } × tag 𝐶 ) )
25 df-bj-2upl ⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
26 df-bj-1upl ⊢ ⦅ 𝐴 ⦆ = ( { ∅ } × tag 𝐴 )
27 26 uneq1i ⊢ ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) = ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) )
28 25 27 eqtri ⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) )
29 28 difeq1i ⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ( { ∅ } × tag 𝐶 ) ) = ( ( ( { ∅ } × tag 𝐴 ) ∪ ( { 1o } × tag 𝐵 ) ) ∖ ( { ∅ } × tag 𝐶 ) )
30 24 29 sseqtrri ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ( { ∅ } × tag 𝐶 ) )
31 df-bj-1upl ⊢ ⦅ 𝐶 ⦆ = ( { ∅ } × tag 𝐶 )
32 31 difeq2i ⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) = ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ( { ∅ } × tag 𝐶 ) )
33 30 32 sseqtrri ⊢ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ )
34 psssstr ⊢ ( ( ∅ ⊊ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ∧ ( ( { 1o } × tag 𝐵 ) ∖ ( ( { ∅ } × tag 𝐴 ) ∪ ( { ∅ } × tag 𝐶 ) ) ) ⊆ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) ) → ∅ ⊊ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) )
35 17 33 34 mp2an ⊢ ∅ ⊊ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ )
36 0pss ⊢ ( ∅ ⊊ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) ↔ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) ≠ ∅ )
37 35 36 mpbi ⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) ≠ ∅
38 difn0 ⊢ ( ( ⦅ 𝐴 , 𝐵 ⦆ ∖ ⦅ 𝐶 ⦆ ) ≠ ∅ → ⦅ 𝐴 , 𝐵 ⦆ ≠ ⦅ 𝐶 ⦆ )
39 37 38 ax-mp ⊢ ⦅ 𝐴 , 𝐵 ⦆ ≠ ⦅ 𝐶 ⦆