Theorem phplem3

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998)

	Ref	Expression
Hypotheses	phplem2.1	$$⊢A\in \mathrm{V}$$
	phplem2.2	$$⊢B\in \mathrm{V}$$
Assertion	phplem3	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{suc}A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		phplem2.1	$$⊢A\in \mathrm{V}$$
2		phplem2.2	$$⊢B\in \mathrm{V}$$
3		elsuci	$$⊢B\in \mathrm{suc}A\to \left(B\in A\vee B=A\right)$$
4	1 2	phplem2	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
5	1	enref	$$⊢A\approx A$$
6		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
7		orddif	$$⊢\mathrm{Ord}A\to A=\mathrm{suc}A\setminus \left\{A\right\}$$
8	6 7	syl	$$⊢A\in \mathrm{\omega }\to A=\mathrm{suc}A\setminus \left\{A\right\}$$
9		sneq	$$⊢A=B\to \left\{A\right\}=\left\{B\right\}$$
10	9	difeq2d	$$⊢A=B\to \mathrm{suc}A\setminus \left\{A\right\}=\mathrm{suc}A\setminus \left\{B\right\}$$
11	10	eqcoms	$$⊢B=A\to \mathrm{suc}A\setminus \left\{A\right\}=\mathrm{suc}A\setminus \left\{B\right\}$$
12	8 11	sylan9eq	$$⊢\left(A\in \mathrm{\omega }\wedge B=A\right)\to A=\mathrm{suc}A\setminus \left\{B\right\}$$
13	5 12	breqtrid	$$⊢\left(A\in \mathrm{\omega }\wedge B=A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
14	4 13	jaodan	$$⊢\left(A\in \mathrm{\omega }\wedge \left(B\in A\vee B=A\right)\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
15	3 14	sylan2	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{suc}A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$