Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of a natural number M , then A with an element removed is equinumerous to M . For a proof with fewer symbols using ax-pow , see dif1enALT . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024)

Ref Expression
Assertion dif1en 
|- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M )
2 19.41v 
 |-  ( E. f ( f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. _om ) ) <-> ( E. f f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. _om ) ) )
3 3anass 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) <-> ( f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. _om ) ) )
4 3 exbii 
 |-  ( E. f ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) <-> E. f ( f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. _om ) ) )
5 3anass 
 |-  ( ( E. f f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) <-> ( E. f f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. _om ) ) )
6 2 4 5 3bitr4i 
 |-  ( E. f ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) <-> ( E. f f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) )
7 sucidg 
 |-  ( M e. _om -> M e. suc M )
8 f1ocnvdm 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' f ` M ) e. A )
9 8 3adant2 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( `' f ` M ) e. A )
10 f1ofvswap 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ ( `' f ` M ) e. A ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
11 9 10 syld3an3 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
12 f1ocnvfv2 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( f ` ( `' f ` M ) ) = M )
13 12 opeq2d 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> <. X , ( f ` ( `' f ` M ) ) >. = <. X , M >. )
14 13 preq1d 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } = { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } )
15 14 uneq2d 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } ) = ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) )
16 15 f1oeq1d 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M <-> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M ) )
17 16 3adant2 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , ( f ` ( `' f ` M ) ) >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M <-> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M ) )
18 11 17 mpbid 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
19 f1ofun 
 |-  ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M -> Fun ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) )
20 opex 
 |-  <. X , M >. e. _V
21 20 prid1 
 |-  <. X , M >. e. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. }
22 elun2 
 |-  ( <. X , M >. e. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } -> <. X , M >. e. ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) )
23 21 22 ax-mp 
 |-  <. X , M >. e. ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } )
24 funopfv 
 |-  ( Fun ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) -> ( <. X , M >. e. ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M ) )
25 23 24 mpi 
 |-  ( Fun ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M )
26 18 19 25 3syl 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M )
27 simp2 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> X e. A )
28 f1ocnvfv 
 |-  ( ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M /\ X e. A ) -> ( ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M -> ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) = X ) )
29 18 27 28 syl2anc 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M -> ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) = X ) )
30 26 29 mpd 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) = X )
31 7 30 syl3an3 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) = X )
32 31 sneqd 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } = { X } )
33 32 difeq2d 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) = ( A \ { X } ) )
34 vex 
 |-  f e. _V
35 34 resex 
 |-  ( f |` ( A \ { X , ( `' f ` M ) } ) ) e. _V
36 prex 
 |-  { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } e. _V
37 35 36 unex 
 |-  ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) e. _V
38 simp3 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> M e. _om )
39 7 18 syl3an3 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
40 dif1enlem 
 |-  ( ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) e. _V /\ M e. _om /\ ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) ~~ M )
41 37 38 39 40 mp3an2i 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) ~~ M )
42 33 41 eqbrtrrd 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( A \ { X } ) ~~ M )
43 42 exlimiv 
 |-  ( E. f ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( A \ { X } ) ~~ M )
44 6 43 sylbir 
 |-  ( ( E. f f : A -1-1-onto-> suc M /\ X e. A /\ M e. _om ) -> ( A \ { X } ) ~~ M )
45 1 44 syl3an1b 
 |-  ( ( A ~~ suc M /\ X e. A /\ M e. _om ) -> ( A \ { X } ) ~~ M )
46 45 3comr 
 |-  ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )