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

Proof

Step Hyp Ref Expression
1 bren A suc M f f : A 1-1 onto suc M
2 19.41v f f : A 1-1 onto suc M X A M ω f f : A 1-1 onto suc M X A M ω
3 3anass f : A 1-1 onto suc M X A M ω f : A 1-1 onto suc M X A M ω
4 3 exbii f f : A 1-1 onto suc M X A M ω f f : A 1-1 onto suc M X A M ω
5 3anass f f : A 1-1 onto suc M X A M ω f f : A 1-1 onto suc M X A M ω
6 2 4 5 3bitr4i f f : A 1-1 onto suc M X A M ω f f : A 1-1 onto suc M X A M ω
7 sucidg M ω M suc M
8 f1ocnvdm f : A 1-1 onto suc M M suc M f -1 M A
9 8 3adant2 f : A 1-1 onto suc M X A M suc M f -1 M A
10 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
11 9 10 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
12 f1ocnvfv2 f : A 1-1 onto suc M M suc M f f -1 M = M
13 12 opeq2d f : A 1-1 onto suc M M suc M X f f -1 M = X M
14 13 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
15 14 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
16 15 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
17 16 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
18 11 17 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
19 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
20 opex X M V
21 20 prid1 X M X M f -1 M f X
22 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
23 21 22 ax-mp X M f A X f -1 M X M f -1 M f X
24 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
25 23 24 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
26 18 19 25 3syl 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 X = M
27 simp2 f : A 1-1 onto suc M X A M suc M X A
28 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
29 18 27 28 syl2anc 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 X = M f A X f -1 M X M f -1 M f X -1 M = X
30 26 29 mpd 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 -1 M = X
31 7 30 syl3an3 f : A 1-1 onto suc M X A M ω 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 X A M ω 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 X A M ω A f A X f -1 M X M f -1 M f X -1 M = A X
34 vex f V
35 34 resex f A X f -1 M V
36 prex X M f -1 M f X V
37 35 36 unex f A X f -1 M X M f -1 M f X V
38 simp3 f : A 1-1 onto suc M X A M ω M ω
39 7 18 syl3an3 f : A 1-1 onto suc M X A M ω f A X f -1 M X M f -1 M f X : A 1-1 onto suc M
40 dif1enlem f A X f -1 M X M f -1 M f X V M ω 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
41 37 38 39 40 mp3an2i f : A 1-1 onto suc M X A M ω A f A X f -1 M X M f -1 M f X -1 M M
42 33 41 eqbrtrrd f : A 1-1 onto suc M X A M ω A X M
43 42 exlimiv f f : A 1-1 onto suc M X A M ω A X M
44 6 43 sylbir f f : A 1-1 onto suc M X A M ω A X M
45 1 44 syl3an1b A suc M X A M ω A X M
46 45 3comr M ω A suc M X A A X M