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 
|- (| A ,, B |) =/= (| C |)

Proof

Step Hyp Ref Expression
1 xpundi 
 |-  ( { (/) } X. ( tag A u. tag C ) ) = ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) )
2 1 difeq2i 
 |-  ( ( { 1o } X. tag B ) \ ( { (/) } X. ( tag A u. tag C ) ) ) = ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) )
3 incom 
 |-  ( ( { (/) } X. ( tag A u. tag C ) ) i^i ( { 1o } X. tag B ) ) = ( ( { 1o } X. tag B ) i^i ( { (/) } X. ( tag A u. tag C ) ) )
4 xp01disjl 
 |-  ( ( { (/) } X. ( tag A u. tag C ) ) i^i ( { 1o } X. tag B ) ) = (/)
5 3 4 eqtr3i 
 |-  ( ( { 1o } X. tag B ) i^i ( { (/) } X. ( tag A u. tag C ) ) ) = (/)
6 disjdif2 
 |-  ( ( ( { 1o } X. tag B ) i^i ( { (/) } X. ( tag A u. tag C ) ) ) = (/) -> ( ( { 1o } X. tag B ) \ ( { (/) } X. ( tag A u. tag C ) ) ) = ( { 1o } X. tag B ) )
7 5 6 ax-mp 
 |-  ( ( { 1o } X. tag B ) \ ( { (/) } X. ( tag A u. tag C ) ) ) = ( { 1o } X. tag B )
8 1oex 
 |-  1o e. _V
9 8 snnz 
 |-  { 1o } =/= (/)
10 bj-tagn0 
 |-  tag B =/= (/)
11 9 10 pm3.2i 
 |-  ( { 1o } =/= (/) /\ tag B =/= (/) )
12 xpnz 
 |-  ( ( { 1o } =/= (/) /\ tag B =/= (/) ) <-> ( { 1o } X. tag B ) =/= (/) )
13 11 12 mpbi 
 |-  ( { 1o } X. tag B ) =/= (/)
14 7 13 eqnetri 
 |-  ( ( { 1o } X. tag B ) \ ( { (/) } X. ( tag A u. tag C ) ) ) =/= (/)
15 2 14 eqnetrri 
 |-  ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) =/= (/)
16 0pss 
 |-  ( (/) C. ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) <-> ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) =/= (/) )
17 15 16 mpbir 
 |-  (/) C. ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) )
18 ssun2 
 |-  ( { (/) } X. tag C ) C_ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) )
19 sscon 
 |-  ( ( { (/) } X. tag C ) C_ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) -> ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( ( { 1o } X. tag B ) \ ( { (/) } X. tag C ) ) )
20 18 19 ax-mp 
 |-  ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( ( { 1o } X. tag B ) \ ( { (/) } X. tag C ) )
21 ssun2 
 |-  ( { 1o } X. tag B ) C_ ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) )
22 ssdif 
 |-  ( ( { 1o } X. tag B ) C_ ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) ) -> ( ( { 1o } X. tag B ) \ ( { (/) } X. tag C ) ) C_ ( ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) ) \ ( { (/) } X. tag C ) ) )
23 21 22 ax-mp 
 |-  ( ( { 1o } X. tag B ) \ ( { (/) } X. tag C ) ) C_ ( ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) ) \ ( { (/) } X. tag C ) )
24 20 23 sstri 
 |-  ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) ) \ ( { (/) } X. tag C ) )
25 df-bj-2upl 
 |-  (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) )
26 df-bj-1upl 
 |-  (| A |) = ( { (/) } X. tag A )
27 26 uneq1i 
 |-  ( (| A |) u. ( { 1o } X. tag B ) ) = ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) )
28 25 27 eqtri 
 |-  (| A ,, B |) = ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) )
29 28 difeq1i 
 |-  ( (| A ,, B |) \ ( { (/) } X. tag C ) ) = ( ( ( { (/) } X. tag A ) u. ( { 1o } X. tag B ) ) \ ( { (/) } X. tag C ) )
30 24 29 sseqtrri 
 |-  ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( (| A ,, B |) \ ( { (/) } X. tag C ) )
31 df-bj-1upl 
 |-  (| C |) = ( { (/) } X. tag C )
32 31 difeq2i 
 |-  ( (| A ,, B |) \ (| C |) ) = ( (| A ,, B |) \ ( { (/) } X. tag C ) )
33 30 32 sseqtrri 
 |-  ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( (| A ,, B |) \ (| C |) )
34 psssstr 
 |-  ( ( (/) C. ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) /\ ( ( { 1o } X. tag B ) \ ( ( { (/) } X. tag A ) u. ( { (/) } X. tag C ) ) ) C_ ( (| A ,, B |) \ (| C |) ) ) -> (/) C. ( (| A ,, B |) \ (| C |) ) )
35 17 33 34 mp2an 
 |-  (/) C. ( (| A ,, B |) \ (| C |) )
36 0pss 
 |-  ( (/) C. ( (| A ,, B |) \ (| C |) ) <-> ( (| A ,, B |) \ (| C |) ) =/= (/) )
37 35 36 mpbi 
 |-  ( (| A ,, B |) \ (| C |) ) =/= (/)
38 difn0 
 |-  ( ( (| A ,, B |) \ (| C |) ) =/= (/) -> (| A ,, B |) =/= (| C |) )
39 37 38 ax-mp 
 |-  (| A ,, B |) =/= (| C |)