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 On A suc M X A A X M

Proof

Step Hyp Ref Expression
1 simp1 A suc M X A M On A suc M
2 encv A suc M A V suc M V
3 2 simpld A suc M A V
4 3 3anim1i A suc M X A M On A V X A M On
5 bren A suc M f f : A 1-1 onto suc M
6 sucidg M On M suc M
7 f1ocnvdm f : A 1-1 onto suc M M suc M f -1 M A
8 7 3adant2 f : A 1-1 onto suc M X A M suc M f -1 M A
9 f1ofvswap f : A 1-1 onto suc M X A f -1 M A f A X f -1 M X f f -1 M f -1 M f X : A 1-1 onto suc M
10 8 9 syld3an3 f : A 1-1 onto suc M X A M suc M f A X f -1 M X f f -1 M f -1 M f X : A 1-1 onto suc M
11 f1ocnvfv2 f : A 1-1 onto suc M M suc M f f -1 M = M
12 11 opeq2d f : A 1-1 onto suc M M suc M X f f -1 M = X M
13 12 preq1d f : A 1-1 onto suc M M suc M X f f -1 M f -1 M f X = X M f -1 M f X
14 13 uneq2d f : A 1-1 onto suc M M suc M f A X f -1 M X f f -1 M f -1 M f X = f A X f -1 M X M f -1 M f X
15 14 f1oeq1d f : A 1-1 onto suc M M suc M f A X f -1 M X f f -1 M f -1 M f X : A 1-1 onto suc M f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
16 15 3adant2 f : A 1-1 onto suc M X A M suc M f A X f -1 M X f f -1 M f -1 M f X : A 1-1 onto suc M f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
17 10 16 mpbid f : A 1-1 onto suc M X A M suc M f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
18 6 17 syl3an3 f : A 1-1 onto suc M X A M On f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
19 18 3adant3r1 f : A 1-1 onto suc M A V X A M On f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
20 f1ofun f A X f -1 M X M f -1 M f X : A 1-1 onto suc M Fun f A X f -1 M X M f -1 M f X
21 opex X M V
22 21 prid1 X M X M f -1 M f X
23 elun2 X M X M f -1 M f X X M f A X f -1 M X M f -1 M f X
24 22 23 ax-mp X M f A X f -1 M X M f -1 M f X
25 funopfv Fun f A X f -1 M X M f -1 M f X X M f A X f -1 M X M f -1 M f X f A X f -1 M X M f -1 M f X X = M
26 24 25 mpi Fun f A X f -1 M X M f -1 M f X f A X f -1 M X M f -1 M f X X = M
27 19 20 26 3syl f : A 1-1 onto suc M A V X A M On f A X f -1 M X M f -1 M f X X = M
28 simpr2 f : A 1-1 onto suc M A V X A M On X A
29 f1ocnvfv f A X f -1 M X M f -1 M f X : A 1-1 onto suc M X A f A X f -1 M X M f -1 M f X X = M f A X f -1 M X M f -1 M f X -1 M = X
30 19 28 29 syl2anc f : A 1-1 onto suc M A V X A M On f A X f -1 M X M f -1 M f X X = M f A X f -1 M X M f -1 M f X -1 M = X
31 27 30 mpd f : A 1-1 onto suc M A V X A M On f A X f -1 M X M f -1 M f X -1 M = X
32 31 sneqd f : A 1-1 onto suc M A V X A M On f A X f -1 M X M f -1 M f X -1 M = X
33 32 difeq2d f : A 1-1 onto suc M A V X A M On A f A X f -1 M X M f -1 M f X -1 M = A X
34 simpr1 f : A 1-1 onto suc M A V X A M On A V
35 3simpc A V X A M On X A M On
36 35 anim2i f : A 1-1 onto suc M A V X A M On f : A 1-1 onto suc M X A M On
37 3anass f : A 1-1 onto suc M X A M On f : A 1-1 onto suc M X A M On
38 36 37 sylibr f : A 1-1 onto suc M A V X A M On f : A 1-1 onto suc M X A M On
39 34 38 jca f : A 1-1 onto suc M A V X A M On A V f : A 1-1 onto suc M X A M On
40 simpl A V f : A 1-1 onto suc M X A M On A V
41 simpr3 A V f : A 1-1 onto suc M X A M On M On
42 40 41 jca A V f : A 1-1 onto suc M X A M On A V M On
43 simpr A V f : A 1-1 onto suc M X A M On f : A 1-1 onto suc M X A M On
44 42 43 jca A V f : A 1-1 onto suc M X A M On A V M On f : A 1-1 onto suc M X A M On
45 vex f V
46 45 resex f A X f -1 M V
47 prex X M f -1 M f X V
48 46 47 unex f A X f -1 M X M f -1 M f X V
49 dif1enlem f A X f -1 M X M f -1 M f X V A V M On f A X f -1 M X M f -1 M f X : A 1-1 onto suc M A f A X f -1 M X M f -1 M f X -1 M M
50 48 49 mp3anl1 A V M On f A X f -1 M X M f -1 M f X : A 1-1 onto suc M A f A X f -1 M X M f -1 M f X -1 M M
51 18 50 sylan2 A V M On f : A 1-1 onto suc M X A M On A f A X f -1 M X M f -1 M f X -1 M M
52 39 44 51 3syl f : A 1-1 onto suc M A V X A M On A f A X f -1 M X M f -1 M f X -1 M M
53 33 52 eqbrtrrd f : A 1-1 onto suc M A V X A M On A X M
54 53 ex f : A 1-1 onto suc M A V X A M On A X M
55 54 exlimiv f f : A 1-1 onto suc M A V X A M On A X M
56 5 55 sylbi A suc M A V X A M On A X M
57 1 4 56 sylc A suc M X A M On A X M
58 57 3comr M On A suc M X A A X M