Theorem phplem1

Description: Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998)

	Ref	Expression
Assertion	phplem1	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)=\mathrm{suc}A\setminus \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
2		nordeq	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to A\ne B$$
3		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
4	2 3	syl	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
5	1 4	sylan	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
6		undif4	$$⊢\left\{A\right\}\cap \left\{B\right\}=\varnothing \to \left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)=\left(\left\{A\right\}\cup A\right)\setminus \left\{B\right\}$$
7		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
8	7	equncomi	$$⊢\mathrm{suc}A=\left\{A\right\}\cup A$$
9	8	difeq1i	$$⊢\mathrm{suc}A\setminus \left\{B\right\}=\left(\left\{A\right\}\cup A\right)\setminus \left\{B\right\}$$
10	6 9	eqtr4di	$$⊢\left\{A\right\}\cap \left\{B\right\}=\varnothing \to \left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)=\mathrm{suc}A\setminus \left\{B\right\}$$
11	5 10	syl	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)=\mathrm{suc}A\setminus \left\{B\right\}$$