# 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 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subset {A}\right)\to {B}\prec {A}$

### Proof

Step Hyp Ref Expression
1 isfi ${⊢}{A}\in \mathrm{Fin}↔\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {x}$
2 relen ${⊢}\mathrm{Rel}\approx$
3 2 brrelex1i ${⊢}{A}\approx {x}\to {A}\in \mathrm{V}$
4 pssss ${⊢}{B}\subset {A}\to {B}\subseteq {A}$
5 ssdomg ${⊢}{A}\in \mathrm{V}\to \left({B}\subseteq {A}\to {B}\preccurlyeq {A}\right)$
6 5 imp ${⊢}\left({A}\in \mathrm{V}\wedge {B}\subseteq {A}\right)\to {B}\preccurlyeq {A}$
7 3 4 6 syl2an ${⊢}\left({A}\approx {x}\wedge {B}\subset {A}\right)\to {B}\preccurlyeq {A}$
8 7 adantll ${⊢}\left(\left({x}\in \mathrm{\omega }\wedge {A}\approx {x}\right)\wedge {B}\subset {A}\right)\to {B}\preccurlyeq {A}$
9 bren ${⊢}{A}\approx {x}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{x}$
10 imass2 ${⊢}{B}\subseteq {A}\to {f}\left[{B}\right]\subseteq {f}\left[{A}\right]$
11 4 10 syl ${⊢}{B}\subset {A}\to {f}\left[{B}\right]\subseteq {f}\left[{A}\right]$
12 11 adantl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to {f}\left[{B}\right]\subseteq {f}\left[{A}\right]$
13 pssnel ${⊢}{B}\subset {A}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge ¬{y}\in {B}\right)$
14 eldif ${⊢}{y}\in \left({A}\setminus {B}\right)↔\left({y}\in {A}\wedge ¬{y}\in {B}\right)$
15 f1ofn ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}Fn{A}$
16 difss ${⊢}{A}\setminus {B}\subseteq {A}$
17 fnfvima ${⊢}\left({f}Fn{A}\wedge {A}\setminus {B}\subseteq {A}\wedge {y}\in \left({A}\setminus {B}\right)\right)\to {f}\left({y}\right)\in {f}\left[{A}\setminus {B}\right]$
18 17 3expia ${⊢}\left({f}Fn{A}\wedge {A}\setminus {B}\subseteq {A}\right)\to \left({y}\in \left({A}\setminus {B}\right)\to {f}\left({y}\right)\in {f}\left[{A}\setminus {B}\right]\right)$
19 15 16 18 sylancl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({y}\in \left({A}\setminus {B}\right)\to {f}\left({y}\right)\in {f}\left[{A}\setminus {B}\right]\right)$
20 dff1o3 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}↔\left({f}:{A}\underset{onto}{⟶}{x}\wedge \mathrm{Fun}{{f}}^{-1}\right)$
21 imadif ${⊢}\mathrm{Fun}{{f}}^{-1}\to {f}\left[{A}\setminus {B}\right]={f}\left[{A}\right]\setminus {f}\left[{B}\right]$
22 20 21 simplbiim ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}\left[{A}\setminus {B}\right]={f}\left[{A}\right]\setminus {f}\left[{B}\right]$
23 22 eleq2d ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({f}\left({y}\right)\in {f}\left[{A}\setminus {B}\right]↔{f}\left({y}\right)\in \left({f}\left[{A}\right]\setminus {f}\left[{B}\right]\right)\right)$
24 19 23 sylibd ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({y}\in \left({A}\setminus {B}\right)\to {f}\left({y}\right)\in \left({f}\left[{A}\right]\setminus {f}\left[{B}\right]\right)\right)$
25 n0i ${⊢}{f}\left({y}\right)\in \left({f}\left[{A}\right]\setminus {f}\left[{B}\right]\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing$
26 24 25 syl6 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({y}\in \left({A}\setminus {B}\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing \right)$
27 14 26 syl5bir ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left(\left({y}\in {A}\wedge ¬{y}\in {B}\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing \right)$
28 27 exlimdv ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge ¬{y}\in {B}\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing \right)$
29 28 imp ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge ¬{y}\in {B}\right)\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing$
30 13 29 sylan2 ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to ¬{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing$
31 ssdif0 ${⊢}{f}\left[{A}\right]\subseteq {f}\left[{B}\right]↔{f}\left[{A}\right]\setminus {f}\left[{B}\right]=\varnothing$
32 30 31 sylnibr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to ¬{f}\left[{A}\right]\subseteq {f}\left[{B}\right]$
33 dfpss3 ${⊢}{f}\left[{B}\right]\subset {f}\left[{A}\right]↔\left({f}\left[{B}\right]\subseteq {f}\left[{A}\right]\wedge ¬{f}\left[{A}\right]\subseteq {f}\left[{B}\right]\right)$
34 12 32 33 sylanbrc ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to {f}\left[{B}\right]\subset {f}\left[{A}\right]$
35 imadmrn ${⊢}{f}\left[\mathrm{dom}{f}\right]=\mathrm{ran}{f}$
36 f1odm ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \mathrm{dom}{f}={A}$
37 36 imaeq2d ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}\left[\mathrm{dom}{f}\right]={f}\left[{A}\right]$
38 f1ofo ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}:{A}\underset{onto}{⟶}{x}$
39 forn ${⊢}{f}:{A}\underset{onto}{⟶}{x}\to \mathrm{ran}{f}={x}$
40 38 39 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \mathrm{ran}{f}={x}$
41 35 37 40 3eqtr3a ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}\left[{A}\right]={x}$
42 41 psseq2d ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({f}\left[{B}\right]\subset {f}\left[{A}\right]↔{f}\left[{B}\right]\subset {x}\right)$
43 42 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to \left({f}\left[{B}\right]\subset {f}\left[{A}\right]↔{f}\left[{B}\right]\subset {x}\right)$
44 34 43 mpbid ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to {f}\left[{B}\right]\subset {x}$
45 php ${⊢}\left({x}\in \mathrm{\omega }\wedge {f}\left[{B}\right]\subset {x}\right)\to ¬{x}\approx {f}\left[{B}\right]$
46 44 45 sylan2 ${⊢}\left({x}\in \mathrm{\omega }\wedge \left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\right)\to ¬{x}\approx {f}\left[{B}\right]$
47 f1of1 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{x}\to {f}:{A}\underset{1-1}{⟶}{x}$
48 f1ores ${⊢}\left({f}:{A}\underset{1-1}{⟶}{x}\wedge {B}\subseteq {A}\right)\to \left({{f}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]$
49 47 4 48 syl2an ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to \left({{f}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]$
50 vex ${⊢}{f}\in \mathrm{V}$
51 50 resex ${⊢}{{f}↾}_{{B}}\in \mathrm{V}$
52 f1oeq1 ${⊢}{y}={{f}↾}_{{B}}\to \left({y}:{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]↔\left({{f}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]\right)$
53 51 52 spcev ${⊢}\left({{f}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]$
54 bren ${⊢}{B}\approx {f}\left[{B}\right]↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]$
55 53 54 sylibr ${⊢}\left({{f}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{f}\left[{B}\right]\to {B}\approx {f}\left[{B}\right]$
56 49 55 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to {B}\approx {f}\left[{B}\right]$
57 entr ${⊢}\left({x}\approx {B}\wedge {B}\approx {f}\left[{B}\right]\right)\to {x}\approx {f}\left[{B}\right]$
58 57 expcom ${⊢}{B}\approx {f}\left[{B}\right]\to \left({x}\approx {B}\to {x}\approx {f}\left[{B}\right]\right)$
59 56 58 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\to \left({x}\approx {B}\to {x}\approx {f}\left[{B}\right]\right)$
60 59 adantl ${⊢}\left({x}\in \mathrm{\omega }\wedge \left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\right)\to \left({x}\approx {B}\to {x}\approx {f}\left[{B}\right]\right)$
61 46 60 mtod ${⊢}\left({x}\in \mathrm{\omega }\wedge \left({f}:{A}\underset{1-1 onto}{⟶}{x}\wedge {B}\subset {A}\right)\right)\to ¬{x}\approx {B}$
62 61 exp32 ${⊢}{x}\in \mathrm{\omega }\to \left({f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({B}\subset {A}\to ¬{x}\approx {B}\right)\right)$
63 62 exlimdv ${⊢}{x}\in \mathrm{\omega }\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{x}\to \left({B}\subset {A}\to ¬{x}\approx {B}\right)\right)$
64 9 63 syl5bi ${⊢}{x}\in \mathrm{\omega }\to \left({A}\approx {x}\to \left({B}\subset {A}\to ¬{x}\approx {B}\right)\right)$
65 64 imp31 ${⊢}\left(\left({x}\in \mathrm{\omega }\wedge {A}\approx {x}\right)\wedge {B}\subset {A}\right)\to ¬{x}\approx {B}$
66 entr ${⊢}\left({B}\approx {A}\wedge {A}\approx {x}\right)\to {B}\approx {x}$
67 66 ex ${⊢}{B}\approx {A}\to \left({A}\approx {x}\to {B}\approx {x}\right)$
68 ensym ${⊢}{B}\approx {x}\to {x}\approx {B}$
69 67 68 syl6com ${⊢}{A}\approx {x}\to \left({B}\approx {A}\to {x}\approx {B}\right)$
70 69 ad2antlr ${⊢}\left(\left({x}\in \mathrm{\omega }\wedge {A}\approx {x}\right)\wedge {B}\subset {A}\right)\to \left({B}\approx {A}\to {x}\approx {B}\right)$
71 65 70 mtod ${⊢}\left(\left({x}\in \mathrm{\omega }\wedge {A}\approx {x}\right)\wedge {B}\subset {A}\right)\to ¬{B}\approx {A}$
72 brsdom ${⊢}{B}\prec {A}↔\left({B}\preccurlyeq {A}\wedge ¬{B}\approx {A}\right)$
73 8 71 72 sylanbrc ${⊢}\left(\left({x}\in \mathrm{\omega }\wedge {A}\approx {x}\right)\wedge {B}\subset {A}\right)\to {B}\prec {A}$
74 73 exp31 ${⊢}{x}\in \mathrm{\omega }\to \left({A}\approx {x}\to \left({B}\subset {A}\to {B}\prec {A}\right)\right)$
75 74 rexlimiv ${⊢}\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {x}\to \left({B}\subset {A}\to {B}\prec {A}\right)$
76 1 75 sylbi ${⊢}{A}\in \mathrm{Fin}\to \left({B}\subset {A}\to {B}\prec {A}\right)$
77 76 imp ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subset {A}\right)\to {B}\prec {A}$