Theorem php3

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. (Contributed by NM, 22-Aug-2008) Avoid ax-pow . (Revised by BTernaryTau, 26-Nov-2024)

	Ref	Expression
Assertion	php3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2		bren	⊢ ( 𝐴 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 )
3		pssss	⊢ ( 𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴 )
4		imass2	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
5	3 4	syl	⊢ ( 𝐵 ⊊ 𝐴 → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
6	5	adantl	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
7		pssnel	⊢ ( 𝐵 ⊊ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
8		eldif	⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
9		f1ofn	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 Fn 𝐴 )
10		difss	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
11		fnfvima	⊢ ( ( 𝑓 Fn 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) )
12	11	3expia	⊢ ( ( 𝑓 Fn 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ) )
13	9 10 12	sylancl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ) )
14		dff1o3	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ↔ ( 𝑓 : 𝐴 –onto→ 𝑥 ∧ Fun ◡ 𝑓 ) )
15		imadif	⊢ ( Fun ◡ 𝑓 → ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) )
16	14 15	simplbiim	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) )
17	16	eleq2d	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) ) )
18	13 17	sylibd	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) ) )
19		n0i	⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
20	18 19	syl6	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
21	8 20	syl5bir	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
22	21	exlimdv	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
23	22	imp	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
24	7 23	sylan2	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
25		ssdif0	⊢ ( ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) ↔ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
26	24 25	sylnibr	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ¬ ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) )
27		dfpss3	⊢ ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) ∧ ¬ ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) ) )
28	6 26 27	sylanbrc	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) )
29		imadmrn	⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
30		f1odm	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → dom 𝑓 = 𝐴 )
31	30	imaeq2d	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ 𝐴 ) )
32		f1ofo	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 : 𝐴 –onto→ 𝑥 )
33		forn	⊢ ( 𝑓 : 𝐴 –onto→ 𝑥 → ran 𝑓 = 𝑥 )
34	32 33	syl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ran 𝑓 = 𝑥 )
35	29 31 34	3eqtr3a	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ 𝐴 ) = 𝑥 )
36	35	psseq2d	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) )
37	36	adantr	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) )
38	28 37	mpbid	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊊ 𝑥 )
39		php2	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) → ( 𝑓 “ 𝐵 ) ≺ 𝑥 )
40	38 39	sylan2	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → ( 𝑓 “ 𝐵 ) ≺ 𝑥 )
41		nnfi	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
42		f1of1	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 : 𝐴 –1-1→ 𝑥 )
43		f1ores	⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
44	42 3 43	syl2an	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
45		vex	⊢ 𝑓 ∈ V
46	45	resex	⊢ ( 𝑓 ↾ 𝐵 ) ∈ V
47		f1oeq1	⊢ ( 𝑦 = ( 𝑓 ↾ 𝐵 ) → ( 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) ↔ ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) ) )
48	46 47	spcev	⊢ ( ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) → ∃ 𝑦 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
49		bren	⊢ ( 𝐵 ≈ ( 𝑓 “ 𝐵 ) ↔ ∃ 𝑦 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
50	48 49	sylibr	⊢ ( ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) → 𝐵 ≈ ( 𝑓 “ 𝐵 ) )
51	44 50	syl	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≈ ( 𝑓 “ 𝐵 ) )
52		endom	⊢ ( 𝐵 ≈ ( 𝑓 “ 𝐵 ) → 𝐵 ≼ ( 𝑓 “ 𝐵 ) )
53		sdomdom	⊢ ( ( 𝑓 “ 𝐵 ) ≺ 𝑥 → ( 𝑓 “ 𝐵 ) ≼ 𝑥 )
54		domfi	⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑓 “ 𝐵 ) ≼ 𝑥 ) → ( 𝑓 “ 𝐵 ) ∈ Fin )
55	53 54	sylan2	⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → ( 𝑓 “ 𝐵 ) ∈ Fin )
56	55	3adant2	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → ( 𝑓 “ 𝐵 ) ∈ Fin )
57		domfi	⊢ ( ( ( 𝑓 “ 𝐵 ) ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ) → 𝐵 ∈ Fin )
58	57	3adant3	⊢ ( ( ( 𝑓 “ 𝐵 ) ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → 𝐵 ∈ Fin )
59		domsdomtrfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → 𝐵 ≺ 𝑥 )
60	58 59	syld3an1	⊢ ( ( ( 𝑓 “ 𝐵 ) ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → 𝐵 ≺ 𝑥 )
61	56 60	syld3an1	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≼ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → 𝐵 ≺ 𝑥 )
62	52 61	syl3an2	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≈ ( 𝑓 “ 𝐵 ) ∧ ( 𝑓 “ 𝐵 ) ≺ 𝑥 ) → 𝐵 ≺ 𝑥 )
63	62	3expia	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≈ ( 𝑓 “ 𝐵 ) ) → ( ( 𝑓 “ 𝐵 ) ≺ 𝑥 → 𝐵 ≺ 𝑥 ) )
64	41 51 63	syl2an	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → ( ( 𝑓 “ 𝐵 ) ≺ 𝑥 → 𝐵 ≺ 𝑥 ) )
65	40 64	mpd	⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → 𝐵 ≺ 𝑥 )
66	65	exp32	⊢ ( 𝑥 ∈ ω → ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥 ) ) )
67	66	exlimdv	⊢ ( 𝑥 ∈ ω → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥 ) ) )
68	2 67	syl5bi	⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥 ) ) )
69		ensymfib	⊢ ( 𝑥 ∈ Fin → ( 𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥 ) )
70	69	adantr	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ) → ( 𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥 ) )
71	70	biimp3ar	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥 ) → 𝑥 ≈ 𝐴 )
72		endom	⊢ ( 𝑥 ≈ 𝐴 → 𝑥 ≼ 𝐴 )
73		sdomdom	⊢ ( 𝐵 ≺ 𝑥 → 𝐵 ≼ 𝑥 )
74		domfi	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≼ 𝑥 ) → 𝐵 ∈ Fin )
75	73 74	sylan2	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ) → 𝐵 ∈ Fin )
76	75	3adant3	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴 ) → 𝐵 ∈ Fin )
77		sdomdomtrfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴 ) → 𝐵 ≺ 𝐴 )
78	76 77	syld3an1	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴 ) → 𝐵 ≺ 𝐴 )
79	72 78	syl3an3	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≈ 𝐴 ) → 𝐵 ≺ 𝐴 )
80	71 79	syld3an3	⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥 ) → 𝐵 ≺ 𝐴 )
81	41 80	syl3an1	⊢ ( ( 𝑥 ∈ ω ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥 ) → 𝐵 ≺ 𝐴 )
82	81	3com23	⊢ ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ∧ 𝐵 ≺ 𝑥 ) → 𝐵 ≺ 𝐴 )
83	82	3exp	⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ≺ 𝑥 → 𝐵 ≺ 𝐴 ) ) )
84	68 83	syldd	⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) ) )
85	84	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) )
86	1 85	sylbi	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) )
87	86	imp	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )