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 lemmas phplem1 through phplem4 , nneneq , and this final piece of the proof. (Contributed by NM, 29-May-1998)

		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		vex	$⊢ x \in V$
21	20	sucex	$⊢ suc x \in V$
22	21	difexi	$⊢ suc x ∖ \{y\} \in V$
23		ssdomg	$⊢ suc x ∖ \{y\} \in V \to (B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\}))$
24	22 23	ax-mp	$⊢ B \subseteq suc x ∖ \{y\} \to B ≼ (suc x ∖ \{y\})$
25	12 19 24	syl56	$⊢ \neg y \in B \to (B \subset suc x \to B ≼ (suc x ∖ \{y\}))$
26	25	imp	$⊢ (\neg y \in B \land B \subset suc x) \to B ≼ (suc x ∖ \{y\})$
27		vex	$⊢ y \in V$
28	20 27	phplem3	$⊢ (x \in ω \land y \in suc x) \to x \approx (suc x ∖ \{y\})$
29	28	ensymd	$⊢ (x \in ω \land y \in suc x) \to (suc x ∖ \{y\}) \approx x$
30		domentr	$⊢ (B ≼ (suc x ∖ \{y\}) \land (suc x ∖ \{y\}) \approx x) \to B ≼ x$
31	26 29 30	syl2an	$⊢ ((\neg y \in B \land B \subset suc x) \land (x \in ω \land y \in suc x)) \to B ≼ x$
32	31	exp43	$⊢ \neg y \in B \to (B \subset suc x \to (x \in ω \to (y \in suc x \to B ≼ x)))$
33	32	com4r	$⊢ y \in suc x \to (\neg y \in B \to (B \subset suc x \to (x \in ω \to B ≼ x)))$
34	33	imp	$⊢ (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
35	34	exlimiv	$⊢ \exists y (y \in suc x \land \neg y \in B) \to (B \subset suc x \to (x \in ω \to B ≼ x))$
36	11 35	mpcom	$⊢ B \subset suc x \to (x \in ω \to B ≼ x)$
37		endomtr	$⊢ (suc x \approx B \land B ≼ x) \to suc x ≼ x$
38		sssucid	$⊢ x \subseteq suc x$
39		ssdomg	$⊢ suc x \in V \to (x \subseteq suc x \to x ≼ suc x)$
40	21 38 39	mp2	$⊢ x ≼ suc x$
41		sbth	$⊢ (suc x ≼ x \land x ≼ suc x) \to suc x \approx x$
42	37 40 41	sylancl	$⊢ (suc x \approx B \land B ≼ x) \to suc x \approx x$
43	42	expcom	$⊢ B ≼ x \to (suc x \approx B \to suc x \approx x)$
44		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
45		nnord	$⊢ suc x \in ω \to Ord suc x$
46	44 45	sylbi	$⊢ x \in ω \to Ord suc x$
47	20	sucid	$⊢ x \in suc x$
48		nordeq	$⊢ (Ord suc x \land x \in suc x) \to suc x \neq x$
49	46 47 48	sylancl	$⊢ x \in ω \to suc x \neq x$
50		nneneq	$⊢ (suc x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
51	44 50	sylanb	$⊢ (x \in ω \land x \in ω) \to (suc x \approx x \leftrightarrow suc x = x)$
52	51	anidms	$⊢ x \in ω \to (suc x \approx x \leftrightarrow suc x = x)$
53	52	necon3bbid	$⊢ x \in ω \to (\neg suc x \approx x \leftrightarrow suc x \neq x)$
54	49 53	mpbird	$⊢ x \in ω \to \neg suc x \approx x$
55	43 54	nsyli	$⊢ B ≼ x \to (x \in ω \to \neg suc x \approx B)$
56	36 55	syli	$⊢ B \subset suc x \to (x \in ω \to \neg suc x \approx B)$
57	56	com12	$⊢ x \in ω \to (B \subset suc x \to \neg suc x \approx B)$
58		psseq2	$⊢ A = suc x \to (B \subset A \leftrightarrow B \subset suc x)$
59		breq1	$⊢ A = suc x \to (A \approx B \leftrightarrow suc x \approx B)$
60	59	notbid	$⊢ A = suc x \to (\neg A \approx B \leftrightarrow \neg suc x \approx B)$
61	58 60	imbi12d	$⊢ A = suc x \to ((B \subset A \to \neg A \approx B) \leftrightarrow (B \subset suc x \to \neg suc x \approx B))$
62	57 61	syl5ibrcom	$⊢ x \in ω \to (A = suc x \to (B \subset A \to \neg A \approx B))$
63	62	rexlimiv	$⊢ \exists x \in ω A = suc x \to (B \subset A \to \neg A \approx B)$
64	10 63	syl	$⊢ (A \in ω \land B \subset A) \to (B \subset A \to \neg A \approx B)$
65	64	ex	$⊢ A \in ω \to (B \subset A \to (B \subset A \to \neg A \approx B))$
66	65	pm2.43d	$⊢ A \in ω \to (B \subset A \to \neg A \approx B)$
67	66	imp	$⊢ (A \in ω \land B \subset A) \to \neg A \approx B$

Metamath Proof Explorer

Theorem php

Proof