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 ∧ 𝐵𝐴 ) → 𝐵𝐴 )