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)

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

Proof

Step Hyp Ref Expression
1 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2 relen ⊢ Rel ≈
3 2 brrelex1i ⊢ ( 𝐴 ≈ 𝑥 → 𝐴 ∈ V )
4 pssss ⊢ ( 𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴 )
5 ssdomg ⊢ ( 𝐴 ∈ V → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) )
6 5 imp ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ≼ 𝐴 )
7 3 4 6 syl2an ⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≼ 𝐴 )
8 7 adantll ⊢ ( ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≼ 𝐴 )
9 bren ⊢ ( 𝐴 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 )
10 imass2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
11 4 10 syl ⊢ ( 𝐵 ⊊ 𝐴 → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
12 11 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) )
13 pssnel ⊢ ( 𝐵 ⊊ 𝐴 → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
14 eldif ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
15 f1ofn ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 Fn 𝐴 )
16 difss ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
17 fnfvima ⊢ ( ( 𝑓 Fn 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) )
18 17 3expia ⊢ ( ( 𝑓 Fn 𝐴 ∧ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ) )
19 15 16 18 sylancl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ) )
20 dff1o3 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ↔ ( 𝑓 : 𝐴 –onto→ 𝑥 ∧ Fun ◡ 𝑓 ) )
21 imadif ⊢ ( Fun ◡ 𝑓 → ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) )
22 20 21 simplbiim ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) )
23 22 eleq2d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑓 “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) ) )
24 19 23 sylibd ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) ) )
25 n0i ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
26 24 25 syl6 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
27 14 26 syl5bir ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
28 27 exlimdv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ ) )
29 28 imp ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
30 13 29 sylan2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ¬ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
31 ssdif0 ⊢ ( ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) ↔ ( ( 𝑓 “ 𝐴 ) ∖ ( 𝑓 “ 𝐵 ) ) = ∅ )
32 30 31 sylnibr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ¬ ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) )
33 dfpss3 ⊢ ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( ( 𝑓 “ 𝐵 ) ⊆ ( 𝑓 “ 𝐴 ) ∧ ¬ ( 𝑓 “ 𝐴 ) ⊆ ( 𝑓 “ 𝐵 ) ) )
34 12 32 33 sylanbrc ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) )
35 imadmrn ⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
36 f1odm ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → dom 𝑓 = 𝐴 )
37 36 imaeq2d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ 𝐴 ) )
38 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 : 𝐴 –onto→ 𝑥 )
39 forn ⊢ ( 𝑓 : 𝐴 –onto→ 𝑥 → ran 𝑓 = 𝑥 )
40 38 39 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ran 𝑓 = 𝑥 )
41 35 37 40 3eqtr3a ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑓 “ 𝐴 ) = 𝑥 )
42 41 psseq2d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) )
43 42 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝑓 “ 𝐵 ) ⊊ ( 𝑓 “ 𝐴 ) ↔ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) )
44 34 43 mpbid ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 “ 𝐵 ) ⊊ 𝑥 )
45 php ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 “ 𝐵 ) ⊊ 𝑥 ) → ¬ 𝑥 ≈ ( 𝑓 “ 𝐵 ) )
46 44 45 sylan2 ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → ¬ 𝑥 ≈ ( 𝑓 “ 𝐵 ) )
47 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → 𝑓 : 𝐴 –1-1→ 𝑥 )
48 f1ores ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
49 47 4 48 syl2an ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
50 vex ⊢ 𝑓 ∈ V
51 50 resex ⊢ ( 𝑓 ↾ 𝐵 ) ∈ V
52 f1oeq1 ⊢ ( 𝑦 = ( 𝑓 ↾ 𝐵 ) → ( 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) ↔ ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) ) )
53 51 52 spcev ⊢ ( ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) → ∃ 𝑦 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
54 bren ⊢ ( 𝐵 ≈ ( 𝑓 “ 𝐵 ) ↔ ∃ 𝑦 𝑦 : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) )
55 53 54 sylibr ⊢ ( ( 𝑓 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑓 “ 𝐵 ) → 𝐵 ≈ ( 𝑓 “ 𝐵 ) )
56 49 55 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≈ ( 𝑓 “ 𝐵 ) )
57 entr ⊢ ( ( 𝑥 ≈ 𝐵 ∧ 𝐵 ≈ ( 𝑓 “ 𝐵 ) ) → 𝑥 ≈ ( 𝑓 “ 𝐵 ) )
58 57 expcom ⊢ ( 𝐵 ≈ ( 𝑓 “ 𝐵 ) → ( 𝑥 ≈ 𝐵 → 𝑥 ≈ ( 𝑓 “ 𝐵 ) ) )
59 56 58 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝑥 ≈ 𝐵 → 𝑥 ≈ ( 𝑓 “ 𝐵 ) ) )
60 59 adantl ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → ( 𝑥 ≈ 𝐵 → 𝑥 ≈ ( 𝑓 “ 𝐵 ) ) )
61 46 60 mtod ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊊ 𝐴 ) ) → ¬ 𝑥 ≈ 𝐵 )
62 61 exp32 ⊢ ( 𝑥 ∈ ω → ( 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝑥 ≈ 𝐵 ) ) )
63 62 exlimdv ⊢ ( 𝑥 ∈ ω → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝑥 ≈ 𝐵 ) ) )
64 9 63 syl5bi ⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝑥 ≈ 𝐵 ) ) )
65 64 imp31 ⊢ ( ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝑥 ≈ 𝐵 )
66 entr ⊢ ( ( 𝐵 ≈ 𝐴 ∧ 𝐴 ≈ 𝑥 ) → 𝐵 ≈ 𝑥 )
67 66 ex ⊢ ( 𝐵 ≈ 𝐴 → ( 𝐴 ≈ 𝑥 → 𝐵 ≈ 𝑥 ) )
68 ensym ⊢ ( 𝐵 ≈ 𝑥 → 𝑥 ≈ 𝐵 )
69 67 68 syl6com ⊢ ( 𝐴 ≈ 𝑥 → ( 𝐵 ≈ 𝐴 → 𝑥 ≈ 𝐵 ) )
70 69 ad2antlr ⊢ ( ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) ∧ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ≈ 𝐴 → 𝑥 ≈ 𝐵 ) )
71 65 70 mtod ⊢ ( ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐵 ≈ 𝐴 )
72 brsdom ⊢ ( 𝐵 ≺ 𝐴 ↔ ( 𝐵 ≼ 𝐴 ∧ ¬ 𝐵 ≈ 𝐴 ) )
73 8 71 72 sylanbrc ⊢ ( ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )
74 73 exp31 ⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) ) )
75 74 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) )
76 1 75 sylbi ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴 ) )
77 76 imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )