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	syl5ibr	$⊢ \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	21 22 23	3syl	$⊢ x \in ω \to suc x ∖ \{y\} \in Fin$
25		ssdomfi	$⊢ suc x ∖ \{y\} \in Fin \to (B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\}))$
26	24 25	syl	$⊢ x \in ω \to (B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\}))$
27	20 26	sylan9	$⊢ (\neg y \in B \land x \in ω) \to (B \subset suc x \to B ≼ (suc x ∖ \{y\}))$
28	27	3impia	$⊢ (\neg y \in B \land x \in ω \land B \subset suc x) \to B ≼ (suc x ∖ \{y\})$
29	28	3com23	$⊢ (\neg y \in B \land B \subset suc x \land x \in ω) \to B ≼ (suc x ∖ \{y\})$
30	29	3expa	$⊢ ((\neg y \in B \land B \subset suc x) \land x \in ω) \to B ≼ (suc x ∖ \{y\})$
31	30	adantrr	$⊢ ((\neg y \in B \land B \subset suc x) \land (x \in ω \land y \in suc x)) \to B ≼ (suc x ∖ \{y\})$
32		nnfi	$⊢ x \in ω \to x \in Fin$
33	32	ad2antrl	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to x \in Fin$
34		simpl	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ (suc x ∖ \{y\})$
35		simpr	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to (x \in ω \land y \in suc x)$
36		phplem1	$⊢ (x \in ω \land y \in suc x) \to x \approx (suc x ∖ \{y\})$
37		ensymfib	$⊢ x \in Fin \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
38	32 37	syl	$⊢ x \in ω \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
39	38	adantr	$⊢ (x \in ω \land y \in suc x) \to (x \approx (suc x ∖ \{y\}) \leftrightarrow (suc x ∖ \{y\}) \approx x)$
40	36 39	mpbid	$⊢ (x \in ω \land y \in suc x) \to (suc x ∖ \{y\}) \approx x$
41		endom	$⊢ (suc x ∖ \{y\}) \approx x \to (suc x ∖ \{y\}) ≼ x$
42	40 41	syl	$⊢ (x \in ω \land y \in suc x) \to (suc x ∖ \{y\}) ≼ x$
43		domtrfir	$⊢ (x \in Fin \land B ≼ (suc x ∖ \{y\}) \land (suc x ∖ \{y\}) ≼ x) \to B ≼ x$
44	42 43	syl3an3	$⊢ (x \in Fin \land B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ x$
45	33 34 35 44	syl3anc	$⊢ (B ≼ (suc x ∖ \{y\}) \land (x \in ω \land y \in suc x)) \to B ≼ x$
46	31 45	sylancom	$⊢ ((\neg y \in B \land B \subset suc x) \land (x \in ω \land y \in suc x)) \to B ≼ x$
47	46	exp43	$⊢ \neg y \in B \to (B \subset suc x \to (x \in ω \to (y \in suc x \to B ≼ x)))$
48	47	com4r	$⊢ y \in suc x \to (\neg y \in B \to (B \subset suc x \to (x \in ω \to B ≼ x)))$
49	48	imp	$⊢ (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
50	49	exlimiv	$⊢ \exists y (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
51	11 50	mpcom	$⊢ B \subset suc x \to (x \in ω \to B ≼ x)$
52		simp1	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to x \in ω$
53		endom	$⊢ suc x \approx B \to suc x ≼ B$
54		domtrfir	$⊢ (x \in Fin \land suc x ≼ B \land B ≼ x) \to suc x ≼ x$
55	53 54	syl3an2	$⊢ (x \in Fin \land suc x \approx B \land B ≼ x) \to suc x ≼ x$
56	32 55	syl3an1	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to suc x ≼ x$
57		sssucid	$⊢ x \subseteq suc x$
58		ssdomfi	$⊢ suc x \in Fin \to (x \subseteq suc x \to x ≼ suc x)$
59	22 57 58	mpisyl	$⊢ suc x \in ω \to x ≼ suc x$
60	21 59	syl	$⊢ x \in ω \to x ≼ suc x$
61	60	adantr	$⊢ (x \in ω \land suc x ≼ x) \to x ≼ suc x$
62		sbthfi	$⊢ (x \in Fin \land suc x ≼ x \land x ≼ suc x) \to suc x \approx x$
63	32 62	syl3an1	$⊢ (x \in ω \land suc x ≼ x \land x ≼ suc x) \to suc x \approx x$
64	61 63	mpd3an3	$⊢ (x \in ω \land suc x ≼ x) \to suc x \approx x$
65	52 56 64	syl2anc	$⊢ (x \in ω \land suc x \approx B \land B ≼ x) \to suc x \approx x$
66	65	3com23	$⊢ (x \in ω \land B ≼ x \land suc x \approx B) \to suc x \approx x$
67	66	3expia	$⊢ (x \in ω \land B ≼ x) \to (suc x \approx B \to suc x \approx x)$
68		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
69		nnord	$⊢ suc x \in ω \to Ord suc x$
70	68 69	sylbi	$⊢ x \in ω \to Ord suc x$
71		vex	$⊢ x \in V$
72	71	sucid	$⊢ x \in suc x$
73		nordeq	$⊢ (Ord suc x \land x \in suc x) \to suc x \neq x$
74	70 72 73	sylancl	$⊢ x \in ω \to suc x \neq x$
75		nneneq	$⊢ (suc x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
76	68 75	sylanb	$⊢ (x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
77	76	anidms	$⊢ x \in ω \to (suc x \approx x \leftrightarrow suc x = x)$
78	77	necon3bbid	$⊢ x \in ω \to (\neg suc x \approx x \leftrightarrow suc x \neq x)$
79	74 78	mpbird	$⊢ x \in ω \to \neg suc x \approx x$
80	67 79	nsyli	$⊢ (x \in ω \land B ≼ x) \to (x \in ω \to \neg suc x \approx B)$
81	80	expcom	$⊢ B ≼ x \to (x \in ω \to (x \in ω \to \neg suc x \approx B))$
82	81	pm2.43d	$⊢ B ≼ x \to (x \in ω \to \neg suc x \approx B)$
83	51 82	syli	$⊢ B \subset suc x \to (x \in ω \to \neg suc x \approx B)$
84	83	com12	$⊢ x \in ω \to (B \subset suc x \to \neg suc x \approx B)$
85		psseq2	$⊢ A = suc x \to (B \subset A \leftrightarrow B \subset suc x)$
86		breq1	$⊢ A = suc x \to (A \approx B \leftrightarrow suc x \approx B)$
87	86	notbid	$⊢ A = suc x \to (\neg A \approx B \leftrightarrow \neg suc x \approx B)$
88	85 87	imbi12d	$⊢ A = suc x \to ((B \subset A \to \neg A \approx B) \leftrightarrow (B \subset suc x \to \neg suc x \approx B))$
89	84 88	syl5ibrcom	$⊢ x \in ω \to (A = suc x \to (B \subset A \to \neg A \approx B))$
90	89	rexlimiv	$⊢ \exists x \in ω A = suc x \to (B \subset A \to \neg A \approx B)$
91	10 90	syl	$⊢ (A \in ω \land B \subset A) \to (B \subset A \to \neg A \approx B)$
92	91	syldbl2	$⊢ (A \in ω \land B \subset A) \to \neg A \approx B$

Metamath Proof Explorer

Theorem php

Proof