phplem2

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) Avoid ax-pow . (Revised by BTernaryTau, 4-Nov-2024)

		Ref	Expression
	Hypothesis	phplem2.1	$⊢ A \in V$
	Assertion	phplem2	$⊢ (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		bren	$⊢ suc A \approx suc B \leftrightarrow \exists f f : suc A \underset{1-1 onto}{⟶} suc B$
3		f1of1	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f : suc A \underset{1-1}{⟶} suc B$
4		nnfi	$⊢ A \in ω \to A \in Fin$
5		sssucid	$⊢ A \subseteq suc A$
6		f1imaenfi	$⊢ (f : suc A \underset{1-1}{⟶} suc B \land A \subseteq suc A \land A \in Fin) \to f [A] \approx A$
7	5 6	mp3an2	$⊢ (f : suc A \underset{1-1}{⟶} suc B \land A \in Fin) \to f [A] \approx A$
8	3 4 7	syl2anr	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to f [A] \approx A$
9		ensymfib	$⊢ A \in Fin \to (A \approx f [A] \leftrightarrow f [A] \approx A)$
10	4 9	syl	$⊢ A \in ω \to (A \approx f [A] \leftrightarrow f [A] \approx A)$
11	10	adantr	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to (A \approx f [A] \leftrightarrow f [A] \approx A)$
12	8 11	mpbird	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx f [A]$
13		nnord	$⊢ A \in ω \to Ord A$
14		orddif	$⊢ Ord A \to A = suc A ∖ \{A\}$
15	13 14	syl	$⊢ A \in ω \to A = suc A ∖ \{A\}$
16	15	imaeq2d	$⊢ A \in ω \to f [A] = f [suc A ∖ \{A\}]$
17		f1ofn	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f Fn suc A$
18	1	sucid	$⊢ A \in suc A$
19		fnsnfv	$⊢ (f Fn suc A \land A \in suc A) \to \{f (A)\} = f [\{A\}]$
20	17 18 19	sylancl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to \{f (A)\} = f [\{A\}]$
21	20	difeq2d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A] ∖ \{f (A)\} = f [suc A] ∖ f [\{A\}]$
22		imadmrn	$⊢ f [dom f] = ran f$
23	22	eqcomi	$⊢ ran f = f [dom f]$
24		f1ofo	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f : suc A \underset{onto}{⟶} suc B$
25		forn	$⊢ f : suc A \underset{onto}{⟶} suc B \to ran f = suc B$
26	24 25	syl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to ran f = suc B$
27		f1odm	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to dom f = suc A$
28	27	imaeq2d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [dom f] = f [suc A]$
29	23 26 28	3eqtr3a	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to suc B = f [suc A]$
30	29	difeq1d	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to suc B ∖ \{f (A)\} = f [suc A] ∖ \{f (A)\}$
31		dff1o3	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \leftrightarrow (f : suc A \underset{onto}{⟶} suc B \land Fun f^{-1})$
32		imadif	$⊢ Fun f^{-1} \to f [suc A ∖ \{A\}] = f [suc A] ∖ f [\{A\}]$
33	31 32	simplbiim	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A ∖ \{A\}] = f [suc A] ∖ f [\{A\}]$
34	21 30 33	3eqtr4rd	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f [suc A ∖ \{A\}] = suc B ∖ \{f (A)\}$
35	16 34	sylan9eq	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to f [A] = suc B ∖ \{f (A)\}$
36	12 35	breqtrd	$⊢ (A \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx (suc B ∖ \{f (A)\})$
37		fnfvelrn	$⊢ (f Fn suc A \land A \in suc A) \to f (A) \in ran f$
38	17 18 37	sylancl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f (A) \in ran f$
39	25	eleq2d	$⊢ f : suc A \underset{onto}{⟶} suc B \to (f (A) \in ran f \leftrightarrow f (A) \in suc B)$
40	24 39	syl	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to (f (A) \in ran f \leftrightarrow f (A) \in suc B)$
41	38 40	mpbid	$⊢ f : suc A \underset{1-1 onto}{⟶} suc B \to f (A) \in suc B$
42		phplem1	$⊢ (B \in ω \land f (A) \in suc B) \to B \approx (suc B ∖ \{f (A)\})$
43	41 42	sylan2	$⊢ (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to B \approx (suc B ∖ \{f (A)\})$
44		nnfi	$⊢ B \in ω \to B \in Fin$
45		ensymfib	$⊢ B \in Fin \to (B \approx (suc B ∖ \{f (A)\}) \leftrightarrow (suc B ∖ \{f (A)\}) \approx B)$
46	44 45	syl	$⊢ B \in ω \to (B \approx (suc B ∖ \{f (A)\}) \leftrightarrow (suc B ∖ \{f (A)\}) \approx B)$
47	46	adantr	$⊢ (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to (B \approx (suc B ∖ \{f (A)\}) \leftrightarrow (suc B ∖ \{f (A)\}) \approx B)$
48	43 47	mpbid	$⊢ (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B) \to (suc B ∖ \{f (A)\}) \approx B$
49		entrfil	$⊢ (A \in Fin \land A \approx (suc B ∖ \{f (A)\}) \land (suc B ∖ \{f (A)\}) \approx B) \to A \approx B$
50	4 49	syl3an1	$⊢ (A \in ω \land A \approx (suc B ∖ \{f (A)\}) \land (suc B ∖ \{f (A)\}) \approx B) \to A \approx B$
51	48 50	syl3an3	$⊢ (A \in ω \land A \approx (suc B ∖ \{f (A)\}) \land (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B)) \to A \approx B$
52	51	3expa	$⊢ ((A \in ω \land A \approx (suc B ∖ \{f (A)\})) \land (B \in ω \land f : suc A \underset{1-1 onto}{⟶} suc B)) \to A \approx B$
53	36 52	syldanl	$⊢ ((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$
54	53	anandirs	$⊢ ((A \in ω \land B \in ω) \land f : suc A \underset{1-1 onto}{⟶} suc B) \to A \approx B$
55	54	ex	$⊢ (A \in ω \land B \in ω) \to (f : suc A \underset{1-1 onto}{⟶} suc B \to A \approx B)$
56	55	exlimdv	$⊢ (A \in ω \land B \in ω) \to (\exists f f : suc A \underset{1-1 onto}{⟶} suc B \to A \approx B)$
57	2 56	syl5bi	$⊢ (A \in ω \land B \in ω) \to (suc A \approx suc B \to A \approx B)$

Metamath Proof Explorer

Theorem phplem2

Proof