Theorem phplem2

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypotheses	phplem2.1	$$⊢A\in \mathrm{V}$$
	phplem2.2	$$⊢B\in \mathrm{V}$$
Assertion	phplem2	$$⊢\left(A\in \mathrm{\omega }\wedge B\in 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		snex	$$⊢\left\{⟨B,A⟩\right\}\in \mathrm{V}$$
4	2 1	f1osn	$$⊢\left\{⟨B,A⟩\right\}:\left\{B\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
5		f1oen3g	$$⊢\left(\left\{⟨B,A⟩\right\}\in \mathrm{V}\wedge \left\{⟨B,A⟩\right\}:\left\{B\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\right)\to \left\{B\right\}\approx \left\{A\right\}$$
6	3 4 5	mp2an	$$⊢\left\{B\right\}\approx \left\{A\right\}$$
7	1	difexi	$$⊢A\setminus \left\{B\right\}\in \mathrm{V}$$
8	7	enref	$$⊢\left(A\setminus \left\{B\right\}\right)\approx \left(A\setminus \left\{B\right\}\right)$$
9	6 8	pm3.2i	$$⊢\left(\left\{B\right\}\approx \left\{A\right\}\wedge \left(A\setminus \left\{B\right\}\right)\approx \left(A\setminus \left\{B\right\}\right)\right)$$
10		incom	$$⊢\left\{A\right\}\cap \left(A\setminus \left\{B\right\}\right)=\left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}$$
11		difss	$$⊢A\setminus \left\{B\right\}\subseteq A$$
12		ssrin	$$⊢A\setminus \left\{B\right\}\subseteq A\to \left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}\subseteq A\cap \left\{A\right\}$$
13	11 12	ax-mp	$$⊢\left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}\subseteq A\cap \left\{A\right\}$$
14		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
15		orddisj	$$⊢\mathrm{Ord}A\to A\cap \left\{A\right\}=\varnothing$$
16	14 15	syl	$$⊢A\in \mathrm{\omega }\to A\cap \left\{A\right\}=\varnothing$$
17	13 16	sseqtrid	$$⊢A\in \mathrm{\omega }\to \left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}\subseteq \varnothing$$
18		ss0	$$⊢\left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}\subseteq \varnothing \to \left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}=\varnothing$$
19	17 18	syl	$$⊢A\in \mathrm{\omega }\to \left(A\setminus \left\{B\right\}\right)\cap \left\{A\right\}=\varnothing$$
20	10 19	syl5eq	$$⊢A\in \mathrm{\omega }\to \left\{A\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing$$
21		disjdif	$$⊢\left\{B\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing$$
22	20 21	jctil	$$⊢A\in \mathrm{\omega }\to \left(\left\{B\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing \wedge \left\{A\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing \right)$$
23		unen	$$⊢\left(\left(\left\{B\right\}\approx \left\{A\right\}\wedge \left(A\setminus \left\{B\right\}\right)\approx \left(A\setminus \left\{B\right\}\right)\right)\wedge \left(\left\{B\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing \wedge \left\{A\right\}\cap \left(A\setminus \left\{B\right\}\right)=\varnothing \right)\right)\to \left(\left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)\approx \left(\left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)$$
24	9 22 23	sylancr	$$⊢A\in \mathrm{\omega }\to \left(\left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)\approx \left(\left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)$$
25	24	adantr	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left(\left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)\approx \left(\left\{A\right\}\cup \left(A\setminus \left\{B\right\}\right)\right)$$
26		uncom	$$⊢\left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)=\left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}$$
27		difsnid	$$⊢B\in A\to \left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=A$$
28	26 27	syl5eq	$$⊢B\in A\to \left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)=A$$
29	28	adantl	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)=A$$
30		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\}$$
31	25 29 30	3brtr3d	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$