Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of an ordinal M , then A with an element removed is equinumerous to M . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A ~~ suc M /\ X e. A /\ M e. On ) -> A ~~ suc M )
2 encv 
 |-  ( A ~~ suc M -> ( A e. _V /\ suc M e. _V ) )
3 2 simpld 
 |-  ( A ~~ suc M -> A e. _V )
4 3 3anim1i 
 |-  ( ( A ~~ suc M /\ X e. A /\ M e. On ) -> ( A e. _V /\ X e. A /\ M e. On ) )
5 bren 
 |-  ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M )
6 sucidg 
 |-  ( M e. On -> M e. suc M )
7 f1ocnvdm 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' f ` M ) e. A )
8 7 3adant2 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. suc M ) -> ( `' f ` M ) e. A )
9 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 )
10 8 9 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 )
11 f1ocnvfv2 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( f ` ( `' f ` M ) ) = M )
12 11 opeq2d 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> <. X , ( f ` ( `' f ` M ) ) >. = <. X , M >. )
13 12 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 ) >. } )
14 13 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 ) >. } ) )
15 14 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 ) )
16 15 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 ) )
17 10 16 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 )
18 6 17 syl3an3 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
19 18 3adant3r1 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) : A -1-1-onto-> suc M )
20 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 ) >. } ) )
21 opex 
 |-  <. X , M >. e. _V
22 21 prid1 
 |-  <. X , M >. e. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. }
23 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 ) >. } ) )
24 22 23 ax-mp 
 |-  <. X , M >. e. ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } )
25 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 ) )
26 24 25 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 )
27 19 20 26 3syl 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` X ) = M )
28 simpr2 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> X e. A )
29 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 ) )
30 19 28 29 syl2anc 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( ( ( ( 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 ) )
31 27 30 mpd 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) = X )
32 31 sneqd 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } = { X } )
33 32 difeq2d 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) = ( A \ { X } ) )
34 simpr1 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> A e. _V )
35 3simpc 
 |-  ( ( A e. _V /\ X e. A /\ M e. On ) -> ( X e. A /\ M e. On ) )
36 35 anim2i 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. On ) ) )
37 3anass 
 |-  ( ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) <-> ( f : A -1-1-onto-> suc M /\ ( X e. A /\ M e. On ) ) )
38 36 37 sylibr 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) )
39 34 38 jca 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) )
40 simpl 
 |-  ( ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> A e. _V )
41 simpr3 
 |-  ( ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> M e. On )
42 40 41 jca 
 |-  ( ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> ( A e. _V /\ M e. On ) )
43 simpr 
 |-  ( ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) )
44 42 43 jca 
 |-  ( ( A e. _V /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> ( ( A e. _V /\ M e. On ) /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) )
45 vex 
 |-  f e. _V
46 45 resex 
 |-  ( f |` ( A \ { X , ( `' f ` M ) } ) ) e. _V
47 prex 
 |-  { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } e. _V
48 46 47 unex 
 |-  ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) e. _V
49 dif1enlem 
 |-  ( ( ( ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) e. _V /\ A e. _V /\ M e. On ) /\ ( ( 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 )
50 48 49 mp3anl1 
 |-  ( ( ( A e. _V /\ M e. On ) /\ ( ( 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 )
51 18 50 sylan2 
 |-  ( ( ( A e. _V /\ M e. On ) /\ ( f : A -1-1-onto-> suc M /\ X e. A /\ M e. On ) ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) ~~ M )
52 39 44 51 3syl 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( A \ { ( `' ( ( f |` ( A \ { X , ( `' f ` M ) } ) ) u. { <. X , M >. , <. ( `' f ` M ) , ( f ` X ) >. } ) ` M ) } ) ~~ M )
53 33 52 eqbrtrrd 
 |-  ( ( f : A -1-1-onto-> suc M /\ ( A e. _V /\ X e. A /\ M e. On ) ) -> ( A \ { X } ) ~~ M )
54 53 ex 
 |-  ( f : A -1-1-onto-> suc M -> ( ( A e. _V /\ X e. A /\ M e. On ) -> ( A \ { X } ) ~~ M ) )
55 54 exlimiv 
 |-  ( E. f f : A -1-1-onto-> suc M -> ( ( A e. _V /\ X e. A /\ M e. On ) -> ( A \ { X } ) ~~ M ) )
56 5 55 sylbi 
 |-  ( A ~~ suc M -> ( ( A e. _V /\ X e. A /\ M e. On ) -> ( A \ { X } ) ~~ M ) )
57 1 4 56 sylc 
 |-  ( ( A ~~ suc M /\ X e. A /\ M e. On ) -> ( A \ { X } ) ~~ M )
58 57 3comr 
 |-  ( ( M e. On /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )