# 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 . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion dif1en ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\to \left({A}\setminus \left\{{X}\right\}\right)\approx {M}$

### Proof

Step Hyp Ref Expression
1 peano2 ${⊢}{M}\in \mathrm{\omega }\to \mathrm{suc}{M}\in \mathrm{\omega }$
2 breq2 ${⊢}{x}=\mathrm{suc}{M}\to \left({A}\approx {x}↔{A}\approx \mathrm{suc}{M}\right)$
3 2 rspcev ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {x}$
4 isfi ${⊢}{A}\in \mathrm{Fin}↔\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {x}$
5 3 4 sylibr ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\right)\to {A}\in \mathrm{Fin}$
6 1 5 sylan ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\right)\to {A}\in \mathrm{Fin}$
7 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{X}\right\}\in \mathrm{Fin}$
8 isfi ${⊢}{A}\setminus \left\{{X}\right\}\in \mathrm{Fin}↔\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}$
9 7 8 sylib ${⊢}{A}\in \mathrm{Fin}\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}$
10 6 9 syl ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}$
11 10 3adant3 ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}$
12 en2sn ${⊢}\left({X}\in {A}\wedge {x}\in \mathrm{V}\right)\to \left\{{X}\right\}\approx \left\{{x}\right\}$
13 12 elvd ${⊢}{X}\in {A}\to \left\{{X}\right\}\approx \left\{{x}\right\}$
14 nnord ${⊢}{x}\in \mathrm{\omega }\to \mathrm{Ord}{x}$
15 orddisj ${⊢}\mathrm{Ord}{x}\to {x}\cap \left\{{x}\right\}=\varnothing$
16 14 15 syl ${⊢}{x}\in \mathrm{\omega }\to {x}\cap \left\{{x}\right\}=\varnothing$
17 incom ${⊢}\left({A}\setminus \left\{{X}\right\}\right)\cap \left\{{X}\right\}=\left\{{X}\right\}\cap \left({A}\setminus \left\{{X}\right\}\right)$
18 disjdif ${⊢}\left\{{X}\right\}\cap \left({A}\setminus \left\{{X}\right\}\right)=\varnothing$
19 17 18 eqtri ${⊢}\left({A}\setminus \left\{{X}\right\}\right)\cap \left\{{X}\right\}=\varnothing$
20 unen ${⊢}\left(\left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\wedge \left\{{X}\right\}\approx \left\{{x}\right\}\right)\wedge \left(\left({A}\setminus \left\{{X}\right\}\right)\cap \left\{{X}\right\}=\varnothing \wedge {x}\cap \left\{{x}\right\}=\varnothing \right)\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)$
21 20 an4s ${⊢}\left(\left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\wedge \left({A}\setminus \left\{{X}\right\}\right)\cap \left\{{X}\right\}=\varnothing \right)\wedge \left(\left\{{X}\right\}\approx \left\{{x}\right\}\wedge {x}\cap \left\{{x}\right\}=\varnothing \right)\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)$
22 19 21 mpanl2 ${⊢}\left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\wedge \left(\left\{{X}\right\}\approx \left\{{x}\right\}\wedge {x}\cap \left\{{x}\right\}=\varnothing \right)\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)$
23 22 expcom ${⊢}\left(\left\{{X}\right\}\approx \left\{{x}\right\}\wedge {x}\cap \left\{{x}\right\}=\varnothing \right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)\right)$
24 13 16 23 syl2an ${⊢}\left({X}\in {A}\wedge {x}\in \mathrm{\omega }\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)\right)$
25 24 3ad2antl3 ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)\right)$
26 difsnid ${⊢}{X}\in {A}\to \left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}={A}$
27 df-suc ${⊢}\mathrm{suc}{x}={x}\cup \left\{{x}\right\}$
28 27 eqcomi ${⊢}{x}\cup \left\{{x}\right\}=\mathrm{suc}{x}$
29 28 a1i ${⊢}{X}\in {A}\to {x}\cup \left\{{x}\right\}=\mathrm{suc}{x}$
30 26 29 breq12d ${⊢}{X}\in {A}\to \left(\left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)↔{A}\approx \mathrm{suc}{x}\right)$
31 30 3ad2ant3 ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\to \left(\left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)↔{A}\approx \mathrm{suc}{x}\right)$
32 31 adantr ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)↔{A}\approx \mathrm{suc}{x}\right)$
33 ensym ${⊢}{A}\approx \mathrm{suc}{M}\to \mathrm{suc}{M}\approx {A}$
34 entr ${⊢}\left(\mathrm{suc}{M}\approx {A}\wedge {A}\approx \mathrm{suc}{x}\right)\to \mathrm{suc}{M}\approx \mathrm{suc}{x}$
35 peano2 ${⊢}{x}\in \mathrm{\omega }\to \mathrm{suc}{x}\in \mathrm{\omega }$
36 nneneq ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge \mathrm{suc}{x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}\approx \mathrm{suc}{x}↔\mathrm{suc}{M}=\mathrm{suc}{x}\right)$
37 35 36 sylan2 ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}\approx \mathrm{suc}{x}↔\mathrm{suc}{M}=\mathrm{suc}{x}\right)$
38 34 37 syl5ib ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left(\left(\mathrm{suc}{M}\approx {A}\wedge {A}\approx \mathrm{suc}{x}\right)\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)$
39 38 expd ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}\approx {A}\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)\right)$
40 33 39 syl5 ${⊢}\left(\mathrm{suc}{M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left({A}\approx \mathrm{suc}{M}\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)\right)$
41 1 40 sylan ${⊢}\left({M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left({A}\approx \mathrm{suc}{M}\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)\right)$
42 41 imp ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\wedge {A}\approx \mathrm{suc}{M}\right)\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)$
43 42 an32s ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)$
44 43 3adantl3 ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left({A}\approx \mathrm{suc}{x}\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)$
45 32 44 sylbid ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\left(\left({A}\setminus \left\{{X}\right\}\right)\cup \left\{{X}\right\}\right)\approx \left({x}\cup \left\{{x}\right\}\right)\to \mathrm{suc}{M}=\mathrm{suc}{x}\right)$
46 peano4 ${⊢}\left({M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}=\mathrm{suc}{x}↔{M}={x}\right)$
47 46 biimpd ${⊢}\left({M}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}=\mathrm{suc}{x}\to {M}={x}\right)$
48 47 3ad2antl1 ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{M}=\mathrm{suc}{x}\to {M}={x}\right)$
49 25 45 48 3syld ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to {M}={x}\right)$
50 breq2 ${⊢}{M}={x}\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {M}↔\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\right)$
51 50 biimprcd ${⊢}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left({M}={x}\to \left({A}\setminus \left\{{X}\right\}\right)\approx {M}\right)$
52 49 51 sylcom ${⊢}\left(\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\wedge {x}\in \mathrm{\omega }\right)\to \left(\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left({A}\setminus \left\{{X}\right\}\right)\approx {M}\right)$
53 52 rexlimdva ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\to \left(\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\setminus \left\{{X}\right\}\right)\approx {x}\to \left({A}\setminus \left\{{X}\right\}\right)\approx {M}\right)$
54 11 53 mpd ${⊢}\left({M}\in \mathrm{\omega }\wedge {A}\approx \mathrm{suc}{M}\wedge {X}\in {A}\right)\to \left({A}\setminus \left\{{X}\right\}\right)\approx {M}$