phplem4

Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998) (Revised by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Hypotheses	phplem2.1	$⊢ A \in V$
	phplem2.2	$⊢ B \in V$
Assertion	phplem4	$⊢ (A \in ω \land B \in ω) \to (suc A \approx suc B \to A \approx B)$

Proof

Step	Hyp	Ref	Expression
1		phplem2.1	$⊢ A \in V$
2		phplem2.2	$⊢ B \in V$
3		bren	$⊢ suc A \approx suc B \leftrightarrow \exists f f : suc A \underset{1-1 onto}{⟶} suc B$
4		f1of1	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f : suc A \underset{1-1}{⟶} suc B$
5	4	adantl	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to f : suc A \underset{1-1}{⟶} suc B$
6	2	sucex	$⊢ suc B \in V$
7		sssucid	$⊢ A \subseteq suc A$
8		f1imaen2g	$⊢ ((f : suc A \underset{1-1}{⟶} suc B \land suc B \in V) \land (A \subseteq suc A \land A \in V)) \to f [A] \approx A$
9	7 1 8	mpanr12	$⊢ (f : suc A \underset{1-1}{⟶} suc B \land suc B \in V) \to f [A] \approx A$
10	5 6 9	sylancl	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to f [A] \approx A$
11	10	ensymd	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx f [A]$
12		nnord	$⊢ A \in ω \to Ord A$
13		orddif	$⊢ Ord A \to A = suc A ∖ \{A\}$
14	12 13	syl	$⊢ A \in ω \to A = suc A ∖ \{A\}$
15	14	imaeq2d	$⊢ A \in ω \to f [A] = f [suc A ∖ \{A\}]$
16		f1ofn	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f Fn suc A$
17	1	sucid	$⊢ A \in suc A$
18		fnsnfv	$⊢ (f Fn suc A \land A \in suc A) \to \{f (A)\} = f [\{A\}]$
19	16 17 18	sylancl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to \{f (A)\} = f [\{A\}]$
20	19	difeq2d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A] ∖ \{f (A)\} = f [suc A] ∖ f [\{A\}]$
21		imadmrn	$⊢ f [dom f] = ran f$
22	21	eqcomi	$⊢ ran f = f [dom f]$
23		f1ofo	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f : suc A \underset{onto}{⟶} suc B$
24		forn	$⊢ f : suc A \underset{onto}{⟶} suc B \to ran f = suc B$
25	23 24	syl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to ran f = suc B$
26		f1odm	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to dom f = suc A$
27	26	imaeq2d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [dom f] = f [suc A]$
28	22 25 27	3eqtr3a	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to suc B = f [suc A]$
29	28	difeq1d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to suc B ∖ \{f (A)\} = f [suc A] ∖ \{f (A)\}$
30		dff1o3	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \leftrightarrow (f : suc A \underset{onto}{⟶} suc B \land Fun f^{-1})$
31		imadif	$⊢ Fun f^{-1} \to f [suc A ∖ \{A\}] = f [suc A] ∖ f [\{A\}]$
32	30 31	simplbiim	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A ∖ \{A\}] = f [suc A] ∖ f [\{A\}]$
33	20 29 32	3eqtr4rd	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A ∖ \{A\}] = suc B ∖ \{f (A)\}$
34	15 33	sylan9eq	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to f [A] = suc B ∖ \{f (A)\}$
35	11 34	breqtrd	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx (suc B ∖ \{f (A)\})$
36		fnfvelrn	$⊢ (f Fn suc A \land A \in suc A) \to f (A) \in ran f$
37	16 17 36	sylancl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f (A) \in ran f$
38	24	eleq2d	$⊢ f : suc A \underset{onto}{⟶} suc B \to (f (A) \in ran f \leftrightarrow f (A) \in suc B)$
39	23 38	syl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to (f (A) \in ran f \leftrightarrow f (A) \in suc B)$
40	37 39	mpbid	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f (A) \in suc B$
41		fvex	$⊢ f (A) \in V$
42	2 41	phplem3	$⊢ (B \in ω \land f (A) \in suc B) \to B \approx (suc B ∖ \{f (A)\})$
43	40 42	sylan2	$⊢ (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to B \approx (suc B ∖ \{f (A)\})$
44	43	ensymd	$⊢ (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to (suc B ∖ \{f (A)\}) \approx B$
45		entr	$⊢ (A \approx (suc B ∖ \{f (A)\}) \land (suc B ∖ \{f (A)\}) \approx B) \to A \approx B$
46	35 44 45	syl2an	$⊢ ((A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \land (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B)) \to A \approx B$
47	46	anandirs	$⊢ ((A \in ω \land B \in ω) \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx B$
48	47	ex	$⊢ (A \in ω \land B \in ω) \to (f : suc A \underset{1-1 onto}{⟶} suc B \to A \approx B)$
49	48	exlimdv	$⊢ (A \in ω \land B \in ω) \to (\exists f f : suc A \underset{1-1 onto}{⟶} suc B \to A \approx B)$
50	3 49	syl5bi	$⊢ (A \in ω \land B \in ω) \to (suc A \approx suc B \to A \approx B)$

Metamath Proof Explorer

Theorem phplem4

Proof