This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid ⊢ ( 𝑓 : 𝐴 –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 biimtrid ⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥 ) ) )
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 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )