Metamath Proof Explorer

Theorem dju1dif

Description: Adding and subtracting one gives back the original cardinality. Similar to pncan for cardinalities. (Contributed by Mario Carneiro, 18-May-2015) (Revised by Jim Kingdon, 20-Aug-2023)

Ref Expression
Assertion dju1dif 
|- ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { B } ) ~~ A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> A e. V )
2 1oex 
 |-  1o e. _V
3 djuex 
 |-  ( ( A e. V /\ 1o e. _V ) -> ( A |_| 1o ) e. _V )
4 1 2 3 sylancl 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( A |_| 1o ) e. _V )
5 simpr 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> B e. ( A |_| 1o ) )
6 df1o2 
 |-  1o = { (/) }
7 6 xpeq2i 
 |-  ( { 1o } X. 1o ) = ( { 1o } X. { (/) } )
8 0ex 
 |-  (/) e. _V
9 2 8 xpsn 
 |-  ( { 1o } X. { (/) } ) = { <. 1o , (/) >. }
10 7 9 eqtri 
 |-  ( { 1o } X. 1o ) = { <. 1o , (/) >. }
11 ssun2 
 |-  ( { 1o } X. 1o ) C_ ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
12 10 11 eqsstrri 
 |-  { <. 1o , (/) >. } C_ ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
13 opex 
 |-  <. 1o , (/) >. e. _V
14 13 snss 
 |-  ( <. 1o , (/) >. e. ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) <-> { <. 1o , (/) >. } C_ ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) )
15 12 14 mpbir 
 |-  <. 1o , (/) >. e. ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
16 df-dju 
 |-  ( A |_| 1o ) = ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
17 15 16 eleqtrri 
 |-  <. 1o , (/) >. e. ( A |_| 1o )
18 17 a1i 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> <. 1o , (/) >. e. ( A |_| 1o ) )
19 difsnen 
 |-  ( ( ( A |_| 1o ) e. _V /\ B e. ( A |_| 1o ) /\ <. 1o , (/) >. e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { B } ) ~~ ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) )
20 4 5 18 19 syl3anc 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { B } ) ~~ ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) )
21 16 difeq1i 
 |-  ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) = ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ { <. 1o , (/) >. } )
22 xp01disjl 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. 1o ) ) = (/)
23 disj3 
 |-  ( ( ( { (/) } X. A ) i^i ( { 1o } X. 1o ) ) = (/) <-> ( { (/) } X. A ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) ) )
24 22 23 mpbi 
 |-  ( { (/) } X. A ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) )
25 difun2 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ ( { 1o } X. 1o ) ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) )
26 10 difeq2i 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ ( { 1o } X. 1o ) ) = ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ { <. 1o , (/) >. } )
27 24 25 26 3eqtr2i 
 |-  ( { (/) } X. A ) = ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ { <. 1o , (/) >. } )
28 21 27 eqtr4i 
 |-  ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) = ( { (/) } X. A )
29 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. V ) -> ( { (/) } X. A ) ~~ A )
30 8 1 29 sylancr 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( { (/) } X. A ) ~~ A )
31 28 30 eqbrtrid 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) ~~ A )
32 entr 
 |-  ( ( ( ( A |_| 1o ) \ { B } ) ~~ ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) /\ ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) ~~ A ) -> ( ( A |_| 1o ) \ { B } ) ~~ A )
33 20 31 32 syl2anc 
 |-  ( ( A e. V /\ B e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { B } ) ~~ A )