php

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of Enderton p. 134. The theorem is so-called because you can't putn + 1 pigeons inton holes (if each hole holds only one pigeon). The proof consists of phplem1 , phplem2 , nneneq , and this final piece of the proof. (Contributed by NM, 29-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 18-Nov-2024)

		Ref	Expression
	Assertion	php	$⊢ (A \in ω \land B \subset A) \to \neg A \approx B$

Proof

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq B$
2		sspsstr	$⊢ (\emptyset \subseteq B \land B \subset A) \to \emptyset \subset A$
3	1 2	mpan	$⊢ B \subset A \to \emptyset \subset A$
4		0pss	$⊢ \emptyset \subset A \leftrightarrow A \neq \emptyset$
5		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
6	4 5	bitri	$⊢ \emptyset \subset A \leftrightarrow \neg A = \emptyset$
7	3 6	sylib	$⊢ B \subset A \to \neg A = \emptyset$
8		nn0suc	$⊢ A \in ω \to (A = \emptyset \lor \exists x \in ω A = suc x)$
9	8	orcanai	$⊢ (A \in ω \land \neg A = \emptyset) \to \exists x \in ω A = suc x$
10	7 9	sylan2	$⊢ (A \in ω \land B \subset A) \to \exists x \in ω A = suc x$
11		pssnel	$⊢ B \subset suc x \to \exists y (y \in suc x \land \neg y \in B)$
12		pssss	$⊢ B \subset suc x \to B \subseteq suc x$
13		ssdif	$⊢ B \subseteq suc x \to B ∖ \{y\} \subseteq suc x ∖ \{y\}$
14		disjsn	$⊢ B \cap \{y\} = \emptyset \leftrightarrow \neg y \in B$
15		disj3	$⊢ B \cap \{y\} = \emptyset \leftrightarrow B = B ∖ \{y\}$
16	14 15	bitr3i	$⊢ \neg y \in B \leftrightarrow B = B ∖ \{y\}$
17		sseq1	$⊢ B = B ∖ \{y\} \to (B \subseteq suc x ∖ \{y\} \leftrightarrow B ∖ \{y\} \subseteq suc x ∖ \{y\})$
18	16 17	sylbi	$⊢ \neg y \in B \to (B \subseteq suc x ∖ \{y\} \leftrightarrow B ∖ \{y\} \subseteq suc x ∖ \{y\})$
19	13 18	imbitrrid	$⊢ \neg y \in B \to (B \subseteq suc x \to B \subseteq suc x ∖ \{y\})$
20	12 19	syl5	$⊢ \neg y \in B \to (B \subset suc x \to B \subseteq suc x ∖ \{y\})$
21		peano2	$⊢ x \in ω \to suc x \in ω$
22		nnfi	$⊢ suc x \in ω \to suc x \in Fin$
23		diffi	$⊢ suc x \in Fin \to suc x ∖ \{y\} \in Fin$
24		ssdomfi	$⊢ suc x ∖ \{y\} \in Fin \to (B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\}))$
25	21 22 23 24	4syl	$⊢ x \in ω \to (B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\}))$
26	20 25	sylan9	$⊢ (\neg y \in B \land x \in ω) \to (B \subset suc x \to B ≼ (suc x ∖ \{y\}))$
27	26	3impia	$⊢ (\neg y \in B \land x \in ω \land B \subset suc x) \to B ≼ (suc x ∖ \{y\})$
28	27	3com23	$⊢ (\neg y \in B \land B \subset suc x \land x \in ω) \to B ≼ (suc x ∖ \{y\})$
29	28	3expa	$⊢ ((\neg y \in B \land B \subset suc x) \land x \in ω) \to B ≼ (suc x ∖ \{y\})$
30	29	adantrr	$⊢ ((\neg y \in B \land B \subset suc x) \land (x \in ω \land y \in suc x)) \to B ≼ (suc x ∖ \{y\})$
31		nnfi	$⊢ x \in ω \to x \in Fin$
32	31	ad2antrl	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to x \in Fin$
33		simpl	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ (suc x ∖ \{y\})$
34		simpr	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to (x \in ω \land y \in suc x)$
35		phplem1	$⊢ (x \in ω \land y \in suc x) \to x \approx (suc x ∖ \{y\})$
36		ensymfib	$⊢ x \in Fin \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
37	31 36	syl	$⊢ x \in ω \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
38	37	adantr	$⊢ (x \in ω \land y \in suc x) \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
39	35 38	mpbid	$⊢ (x \in ω \land y \in suc x) \to (suc x ∖ \{y\}) \approx x$
40		endom	$⊢ (suc x ∖ \{y\}) \approx x \to (suc x ∖ \{y\}) ≼ x$
41	39 40	syl	$⊢ (x \in ω \land y \in suc x) \to (suc x ∖ \{y\}) ≼ x$
42		domtrfir	$⊢ (x \in Fin \land B ≼ (suc x ∖ \{y\}) \land (suc x ∖ \{y\}) ≼ x) \to B ≼ x$
43	41 42	syl3an3	$⊢ (x \in Fin \land B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ x$
44	32 33 34 43	syl3anc	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ x$
45	30 44	sylancom	$⊢ ((\neg y \in B \land B \subset suc x) \land (x \in ω \land y \in suc x)) \to B ≼ x$
46	45	exp43	$⊢ \neg y \in B \to (B \subset suc x \to (x \in ω \to (y \in suc x \to B ≼ x)))$
47	46	com4r	$⊢ y \in suc x \to (\neg y \in B \to (B \subset suc x \to (x \in ω \to B ≼ x)))$
48	47	imp	$⊢ (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
49	48	exlimiv	$⊢ \exists y (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
50	11 49	mpcom	$⊢ B \subset suc x \to (x \in ω \to B ≼ x)$
51		simp1	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to x \in ω$
52		endom	$⊢ suc x \approx B \to suc x ≼ B$
53		domtrfir	$⊢ (x \in Fin \land suc x ≼ B \land B ≼ x) \to suc x ≼ x$
54	52 53	syl3an2	$⊢ (x \in Fin \land suc x \approx B \land B ≼ x) \to suc x ≼ x$
55	31 54	syl3an1	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to suc x ≼ x$
56		sssucid	$⊢ x \subseteq suc x$
57		ssdomfi	$⊢ suc x \in Fin \to (x \subseteq suc x \to x ≼ suc x)$
58	22 56 57	mpisyl	$⊢ suc x \in ω \to x ≼ suc x$
59	21 58	syl	$⊢ x \in ω \to x ≼ suc x$
60	59	adantr	$⊢ (x \in ω \land suc x ≼ x) \to x ≼ suc x$
61		sbthfi	$⊢ (x \in Fin \land suc x ≼ x \land x ≼ suc x) \to suc x \approx x$
62	31 61	syl3an1	$⊢ (x \in ω \land suc x ≼ x \land x ≼ suc x) \to suc x \approx x$
63	60 62	mpd3an3	$⊢ (x \in ω \land suc x ≼ x) \to suc x \approx x$
64	51 55 63	syl2anc	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to suc x \approx x$
65	64	3com23	$⊢ (x \in ω \land B ≼ x \land suc x \approx B) \to suc x \approx x$
66	65	3expia	$⊢ (x \in ω \land B ≼ x) \to (suc x \approx B \to suc x \approx x)$
67		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
68		nnord	$⊢ suc x \in ω \to Ord suc x$
69	67 68	sylbi	$⊢ x \in ω \to Ord suc x$
70		vex	$⊢ x \in V$
71	70	sucid	$⊢ x \in suc x$
72		nordeq	$⊢ (Ord suc x \land x \in suc x) \to suc x \neq x$
73	69 71 72	sylancl	$⊢ x \in ω \to suc x \neq x$
74		nneneq	$⊢ (suc x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
75	67 74	sylanb	$⊢ (x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
76	75	anidms	$⊢ x \in ω \to (suc x \approx x \leftrightarrow suc x = x)$
77	76	necon3bbid	$⊢ x \in ω \to (\neg suc x \approx x \leftrightarrow suc x \neq x)$
78	73 77	mpbird	$⊢ x \in ω \to \neg suc x \approx x$
79	66 78	nsyli	$⊢ (x \in ω \land B ≼ x) \to (x \in ω \to \neg suc x \approx B)$
80	79	expcom	$⊢ B ≼ x \to (x \in ω \to (x \in ω \to \neg suc x \approx B))$
81	80	pm2.43d	$⊢ B ≼ x \to (x \in ω \to \neg suc x \approx B)$
82	50 81	syli	$⊢ B \subset suc x \to (x \in ω \to \neg suc x \approx B)$
83	82	com12	$⊢ x \in ω \to (B \subset suc x \to \neg suc x \approx B)$
84		psseq2	$⊢ A = suc x \to (B \subset A \leftrightarrow B \subset suc x)$
85		breq1	$⊢ A = suc x \to (A \approx B \leftrightarrow suc x \approx B)$
86	85	notbid	$⊢ A = suc x \to (\neg A \approx B \leftrightarrow \neg suc x \approx B)$
87	84 86	imbi12d	$⊢ A = suc x \to ((B \subset A \to \neg A \approx B) \leftrightarrow (B \subset suc x \to \neg suc x \approx B))$
88	83 87	syl5ibrcom	$⊢ x \in ω \to (A = suc x \to (B \subset A \to \neg A \approx B))$
89	88	rexlimiv	$⊢ \exists x \in ω A = suc x \to (B \subset A \to \neg A \approx B)$
90	10 89	syl	$⊢ (A \in ω \land B \subset A) \to (B \subset A \to \neg A \approx B)$
91	90	syldbl2	$⊢ (A \in ω \land B \subset A) \to \neg A \approx B$

Metamath Proof Explorer

Theorem php

Proof