Theorem phpm 6988

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. By "proper subset" here we mean that there is an element which is in the natural number and not in the subset, or in symbols ∃𝑥𝑥 ∈ (𝐴 ∖ 𝐵) (which is stronger than not being equal in the absence of excluded middle). Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 6974 through phplem4 6977, nneneq 6979, and this final piece of the proof. (Contributed by NM, 29-May-1998.)

Assertion

Ref	Expression
phpm	⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem phpm

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 110	. . . . . 6 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → 𝐴 = ∅)
2		eldifi 3303	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
3		ne0i 3475	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
4	2, 3	syl 14	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝐴 ≠ ∅)
5	4	neneqd 2399	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 = ∅)
6	5	ad2antlr 489	. . . . . 6 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴 = ∅)
7	1, 6	pm2.21dd 621	. . . . 5 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴 ≈ 𝐵)
8		php5dom 6985	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → ¬ suc 𝑦 ≼ 𝑦)
9	8	ad2antlr 489	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ suc 𝑦 ≼ 𝑦)
10		simplr 528	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 = suc 𝑦)
11		simpr 110	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 ≈ 𝐵)
12		vex 2779	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
13	12	sucex 4565	. . . . . . . . . . . . . . 15 ⊢ suc 𝑦 ∈ V
14		difss 3307	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑦 ∖ {𝑥}) ⊆ suc 𝑦
15	13, 14	ssexi 4198	. . . . . . . . . . . . . 14 ⊢ (suc 𝑦 ∖ {𝑥}) ∈ V
16		eldifn 3304	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
17	16	ad3antlr 493	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝑥 ∈ 𝐵)
18		simpllr 534	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) → 𝐵 ⊆ 𝐴)
19	18	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ 𝐴)
20		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐴 = suc 𝑦)
21	19, 20	sseqtrd 3239	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ suc 𝑦)
22		ssdif 3316	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ⊆ suc 𝑦 → (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥}))
23		disjsn 3705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝐵)
24		disj3 3521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∩ {𝑥}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑥}))
25	23, 24	bitr3i 186	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑥}))
26		sseq1 3224	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = (𝐵 ∖ {𝑥}) → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥})))
27	25, 26	sylbi 121	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥})))
28	22, 27	imbitrrid 156	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ 𝐵 → (𝐵 ⊆ suc 𝑦 → 𝐵 ⊆ (suc 𝑦 ∖ {𝑥})))
29	17, 21, 28	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ (suc 𝑦 ∖ {𝑥}))
30		ssdomg 6893	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑦 ∖ {𝑥}) ∈ V → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥})))
31	15, 29, 30	mpsyl 65	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥}))
32		simplr 528	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑦 ∈ ω)
33	2	ad3antlr 493	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥 ∈ 𝐴)
34	33, 20	eleqtrd 2286	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥 ∈ suc 𝑦)
35		phplem3g 6978	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → 𝑦 ≈ (suc 𝑦 ∖ {𝑥}))
36	35	ensymd 6898	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦)
37	32, 34, 36	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦)
38		domentr 6906	. . . . . . . . . . . . 13 ⊢ ((𝐵 ≼ (suc 𝑦 ∖ {𝑥}) ∧ (suc 𝑦 ∖ {𝑥}) ≈ 𝑦) → 𝐵 ≼ 𝑦)
39	31, 37, 38	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ≼ 𝑦)
40	39	adantr 276	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐵 ≼ 𝑦)
41		endomtr 6905	. . . . . . . . . . 11 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝑦) → 𝐴 ≼ 𝑦)
42	11, 40, 41	syl2anc 411	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 ≼ 𝑦)
43	10, 42	eqbrtrrd 4083	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → suc 𝑦 ≼ 𝑦)
44	9, 43	mtand 667	. . . . . . . 8 ⊢ (((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝐴 ≈ 𝐵)
45	44	ex 115	. . . . . . 7 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) → (𝐴 = suc 𝑦 → ¬ 𝐴 ≈ 𝐵))
46	45	rexlimdva 2625	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (∃𝑦 ∈ ω 𝐴 = suc 𝑦 → ¬ 𝐴 ≈ 𝐵))
47	46	imp 124	. . . . 5 ⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ ∃𝑦 ∈ ω 𝐴 = suc 𝑦) → ¬ 𝐴 ≈ 𝐵)
48		nn0suc 4670	. . . . . 6 ⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦))
49	48	ad2antrr 488	. . . . 5 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦))
50	7, 47, 49	mpjaodan 800	. . . 4 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵)
51	50	ex 115	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 ≈ 𝐵))
52	51	exlimdv 1843	. 2 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 ≈ 𝐵))
53	52	3impia 1203	1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 710   ∧ w3a 981   = wceq 1373  ∃wex 1516   ∈ wcel 2178   ≠ wne 2378  ∃wrex 2487  Vcvv 2776   ∖ cdif 3171   ∩ cin 3173   ⊆ wss 3174  ∅c0 3468  {csn 3643   class class class wbr 4059  suc csuc 4430  ωcom 4656   ≈ cen 6848   ≼ cdom 6849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-nul 4186  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-iinf 4654

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-nul 3469  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-tr 4159  df-id 4358  df-iord 4431  df-on 4433  df-suc 4436  df-iom 4657  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297  df-fv 5298  df-er 6643  df-en 6851  df-dom 6852

This theorem is referenced by:  phpelm  6989