Theorem php3 3411

Description: Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A, the B is strictly less numerous than A. Stronger version of Corollary 6C of [Enderton] p. 135. (The expression ∃x ∈ ωA ≈ x is the definition of "finite", and "infinite" is defined as "not finite".)

Assertion

Ref	Expression
php3	⊢ ((∃x ∈ ω A ≈ x ∧ B ⊂ A) → B ≺ A)

Distinct variable group(s):   x,A

Proof of Theorem php3

Step	Hyp	Ref	Expression
1		ssdom2g 3312	. . . . . . . . . 10 ⊢ (A ∈ V → (B ⊆ A → B ≼ A))
2	1	imp 277	. . . . . . . . 9 ⊢ ((A ∈ V ∧ B ⊆ A) → B ≼ A)
3		relen 3277	. . . . . . . . . 10 ⊢ Rel ≈
4	3	brrelexi 2447	. . . . . . . . 9 ⊢ (A ≈ z → A ∈ V)
5		pssss 1567	. . . . . . . . 9 ⊢ (B ⊂ A → B ⊆ A)
6	2, 4, 5	syl2an 349	. . . . . . . 8 ⊢ ((A ≈ z ∧ B ⊂ A) → B ≼ A)
7	6	adantll 309	. . . . . . 7 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → B ≼ A)
8		php 3409	. . . . . . . . . . . . . 14 ⊢ ((z ∈ ω ∧ (f “ B) ⊂ z) → ¬ z ≈ (f “ B))
9		imass2 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (B ⊆ A → (f “ B) ⊆ (f “ A))
10	5, 9	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ (B ⊂ A → (f “ B) ⊆ (f “ A))
11	10	adantl 305	. . . . . . . . . . . . . . . . 17 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → (f “ B) ⊆ (f “ A))
12		funfvima2 2905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Fun f ∧ (A ∖ B) ⊆ dom f) → (y ∈ (A ∖ B) → (f ‘y) ∈ (f “ (A ∖ B))))
13		f1ofun 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:A–1-1-onto→z → Fun f)
14		difss 1596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (A ∖ B) ⊆ A
15		f1ofn 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:A–1-1-onto→z → f Fn A)
16		fndm 2723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f Fn A → dom f = A)
17		sseq2 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (dom f = A → ((A ∖ B) ⊆ dom f ↔ (A ∖ B) ⊆ A))
18	15, 16, 17	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:A–1-1-onto→z → ((A ∖ B) ⊆ dom f ↔ (A ∖ B) ⊆ A))
19	14, 18	mpbiri 169	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:A–1-1-onto→z → (A ∖ B) ⊆ dom f)
20	12, 13, 19	sylanc 361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:A–1-1-onto→z → (y ∈ (A ∖ B) → (f ‘y) ∈ (f “ (A ∖ B))))
21		f1o3 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (f:A–1-1-onto→z ↔ (f:A–onto→z ∧ Fun ◡f))
22	21	pm3.27bd 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:A–1-1-onto→z → Fun ◡f)
23		imadif 2714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Fun ◡f → (f “ (A ∖ B)) = ((f “ A) ∖ (f “ B)))
24	22, 23	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:A–1-1-onto→z → (f “ (A ∖ B)) = ((f “ A) ∖ (f “ B)))
25	24	eleq2d 1156	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:A–1-1-onto→z → ((f ‘y) ∈ (f “ (A ∖ B)) ↔ (f ‘y) ∈ ((f “ A) ∖ (f “ B))))
26	20, 25	sylibd 177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:A–1-1-onto→z → (y ∈ (A ∖ B) → (f ‘y) ∈ ((f “ A) ∖ (f “ B))))
27		n0i 1712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f ‘y) ∈ ((f “ A) ∖ (f “ B)) → ¬ ((f “ A) ∖ (f “ B)) = ∅)
28	26, 27	syl6 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:A–1-1-onto→z → (y ∈ (A ∖ B) → ¬ ((f “ A) ∖ (f “ B)) = ∅))
29		eldif 1496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ∈ (A ∖ B) ↔ (y ∈ A ∧ ¬ y ∈ B))
30	28, 29	syl5ibr 182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f:A–1-1-onto→z → ((y ∈ A ∧ ¬ y ∈ B) → ¬ ((f “ A) ∖ (f “ B)) = ∅))
31	30	19.23adv 954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f:A–1-1-onto→z → (∃y(y ∈ A ∧ ¬ y ∈ B) → ¬ ((f “ A) ∖ (f “ B)) = ∅))
32	31	imp 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f:A–1-1-onto→z ∧ ∃y(y ∈ A ∧ ¬ y ∈ B)) → ¬ ((f “ A) ∖ (f “ B)) = ∅)
33		pssnel 1752	. . . . . . . . . . . . . . . . . . 19 ⊢ (B ⊂ A → ∃y(y ∈ A ∧ ¬ y ∈ B))
34	32, 33	sylan2 346	. . . . . . . . . . . . . . . . . 18 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → ¬ ((f “ A) ∖ (f “ B)) = ∅)
35		ssdif0 1748	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f “ A) ⊆ (f “ B) ↔ ((f “ A) ∖ (f “ B)) = ∅)
36	35	negbii 162	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (f “ A) ⊆ (f “ B) ↔ ¬ ((f “ A) ∖ (f “ B)) = ∅)
37	34, 36	sylibr 175	. . . . . . . . . . . . . . . . 17 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → ¬ (f “ A) ⊆ (f “ B))
38	11, 37	jca 236	. . . . . . . . . . . . . . . 16 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → ((f “ B) ⊆ (f “ A) ∧ ¬ (f “ A) ⊆ (f “ B)))
39		dfpss3 1558	. . . . . . . . . . . . . . . 16 ⊢ ((f “ B) ⊂ (f “ A) ↔ ((f “ B) ⊆ (f “ A) ∧ ¬ (f “ A) ⊆ (f “ B)))
40	38, 39	sylibr 175	. . . . . . . . . . . . . . 15 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → (f “ B) ⊂ (f “ A))
41		imadmrn 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ (f “ dom f) = ran f
42	41	a1i 7	. . . . . . . . . . . . . . . . . 18 ⊢ (f:A–1-1-onto→z → (f “ dom f) = ran f)
43		imaeq2 2603	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom f = A → (f “ dom f) = (f “ A))
44	15, 16, 43	3syl 21	. . . . . . . . . . . . . . . . . 18 ⊢ (f:A–1-1-onto→z → (f “ dom f) = (f “ A))
45		f1ofo 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:A–1-1-onto→z → f:A–onto→z)
46		forn 2789	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:A–onto→z → ran f = z)
47	45, 46	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ (f:A–1-1-onto→z → ran f = z)
48	42, 44, 47	3eqtr3d 1133	. . . . . . . . . . . . . . . . 17 ⊢ (f:A–1-1-onto→z → (f “ A) = z)
49	48	psseq2d 1565	. . . . . . . . . . . . . . . 16 ⊢ (f:A–1-1-onto→z → ((f “ B) ⊂ (f “ A) ↔ (f “ B) ⊂ z))
50	49	adantr 306	. . . . . . . . . . . . . . 15 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → ((f “ B) ⊂ (f “ A) ↔ (f “ B) ⊂ z))
51	40, 50	mpbid 170	. . . . . . . . . . . . . 14 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → (f “ B) ⊂ z)
52	8, 51	sylan2 346	. . . . . . . . . . . . 13 ⊢ ((z ∈ ω ∧ (f:A–1-1-onto→z ∧ B ⊂ A)) → ¬ z ≈ (f “ B))
53		f1ores 2813	. . . . . . . . . . . . . . . 16 ⊢ ((f:A–1-1→z ∧ B ⊆ A) → (f ↾ B):B–1-1-onto→(f “ B))
54		f1of1 2799	. . . . . . . . . . . . . . . 16 ⊢ (f:A–1-1-onto→z → f:A–1-1→z)
55	53, 54, 5	syl2an 349	. . . . . . . . . . . . . . 15 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → (f ↾ B):B–1-1-onto→(f “ B))
56		visset 1350	. . . . . . . . . . . . . . . . . 18 ⊢ f ∈ V
57		resexg 2597	. . . . . . . . . . . . . . . . . 18 ⊢ (f ∈ V → (f ↾ B) ∈ V)
58	56, 57	ax-mp 6	. . . . . . . . . . . . . . . . 17 ⊢ (f ↾ B) ∈ V
59		f1oeq1 2795	. . . . . . . . . . . . . . . . 17 ⊢ (y = (f ↾ B) → (y:B–1-1-onto→(f “ B) ↔ (f ↾ B):B–1-1-onto→(f “ B)))
60	58, 59	cla4ev 1401	. . . . . . . . . . . . . . . 16 ⊢ ((f ↾ B):B–1-1-onto→(f “ B) → ∃y y:B–1-1-onto→(f “ B))
61		imaexg 2612	. . . . . . . . . . . . . . . . . 18 ⊢ (f ∈ V → (f “ B) ∈ V)
62	56, 61	ax-mp 6	. . . . . . . . . . . . . . . . 17 ⊢ (f “ B) ∈ V
63	62	bren 3282	. . . . . . . . . . . . . . . 16 ⊢ (B ≈ (f “ B) ↔ ∃y y:B–1-1-onto→(f “ B))
64	60, 63	sylibr 175	. . . . . . . . . . . . . . 15 ⊢ ((f ↾ B):B–1-1-onto→(f “ B) → B ≈ (f “ B))
65		entrt 3319	. . . . . . . . . . . . . . . . 17 ⊢ ((z ≈ B ∧ B ≈ (f “ B)) → z ≈ (f “ B))
66	65	exp 291	. . . . . . . . . . . . . . . 16 ⊢ (z ≈ B → (B ≈ (f “ B) → z ≈ (f “ B)))
67	66	com12 13	. . . . . . . . . . . . . . 15 ⊢ (B ≈ (f “ B) → (z ≈ B → z ≈ (f “ B)))
68	55, 64, 67	3syl 21	. . . . . . . . . . . . . 14 ⊢ ((f:A–1-1-onto→z ∧ B ⊂ A) → (z ≈ B → z ≈ (f “ B)))
69	68	adantl 305	. . . . . . . . . . . . 13 ⊢ ((z ∈ ω ∧ (f:A–1-1-onto→z ∧ B ⊂ A)) → (z ≈ B → z ≈ (f “ B)))
70	52, 69	mtod 95	. . . . . . . . . . . 12 ⊢ ((z ∈ ω ∧ (f:A–1-1-onto→z ∧ B ⊂ A)) → ¬ z ≈ B)
71	70	exp32 294	. . . . . . . . . . 11 ⊢ (z ∈ ω → (f:A–1-1-onto→z → (B ⊂ A → ¬ z ≈ B)))
72	71	19.23adv 954	. . . . . . . . . 10 ⊢ (z ∈ ω → (∃f f:A–1-1-onto→z → (B ⊂ A → ¬ z ≈ B)))
73		visset 1350	. . . . . . . . . . 11 ⊢ z ∈ V
74	73	bren 3282	. . . . . . . . . 10 ⊢ (A ≈ z ↔ ∃f f:A–1-1-onto→z)
75	72, 74	syl5ib 181	. . . . . . . . 9 ⊢ (z ∈ ω → (A ≈ z → (B ⊂ A → ¬ z ≈ B)))
76	75	imp31 280	. . . . . . . 8 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → ¬ z ≈ B)
77		entrt 3319	. . . . . . . . . . . 12 ⊢ ((B ≈ A ∧ A ≈ z) → B ≈ z)
78	77	exp 291	. . . . . . . . . . 11 ⊢ (B ≈ A → (A ≈ z → B ≈ z))
79	73	ensym 3317	. . . . . . . . . . 11 ⊢ (B ≈ z → z ≈ B)
80	78, 79	syl6 23	. . . . . . . . . 10 ⊢ (B ≈ A → (A ≈ z → z ≈ B))
81	80	com12 13	. . . . . . . . 9 ⊢ (A ≈ z → (B ≈ A → z ≈ B))
82	81	ad2antlr 321	. . . . . . . 8 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → (B ≈ A → z ≈ B))
83	76, 82	mtod 95	. . . . . . 7 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → ¬ B ≈ A)
84	7, 83	jca 236	. . . . . 6 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → (B ≼ A ∧ ¬ B ≈ A))
85		brsdom 3286	. . . . . 6 ⊢ (B ≺ A ↔ (B ≼ A ∧ ¬ B ≈ A))
86	84, 85	sylibr 175	. . . . 5 ⊢ (((z ∈ ω ∧ A ≈ z) ∧ B ⊂ A) → B ≺ A)
87	86	exp31 293	. . . 4 ⊢ (z ∈ ω → (A ≈ z → (B ⊂ A → B ≺ A)))
88	87	r19.23aiv 1284	. . 3 ⊢ (∃z ∈ ω A ≈ z → (B ⊂ A → B ≺ A))
89	88	imp 277	. 2 ⊢ ((∃z ∈ ω A ≈ z ∧ B ⊂ A) → B ≺ A)
90		breq2 2066	. . 3 ⊢ (x = z → (A ≈ x ↔ A ≈ z))
91	90	cbvrexv 1334	. 2 ⊢ (∃x ∈ ω A ≈ x ↔ ∃z ∈ ω A ≈ z)
92	89, 91	sylanb 344	1 ⊢ ((∃x ∈ ω A ≈ x ∧ B ⊂ A) → B ≺ A)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707   class class class wbr 2054  ωcom 2372  ^◡ccnv 2409  dom cdm 2410  ran crn 2411   ↾ cres 2412   “ cima 2413  Fun wfun 2416   Fn wfn 2417  –1-1→wf1 2419  –onto→wfo 2420  –1-1-onto→wf1o 2421   ‘cfv 2422   ≈ cen 3271   ≼ cdom 3272   ≺ csdm 3273

This theorem is referenced by:  pssinf 3422

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-er 3200  df-en 3274  df-dom 3275  df-sdom 3276

metamath.org