Description: Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010) (Revised by Mario Carneiro, 27-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | f1finf1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | f1f | |
|
3 | 2 | adantl | |
4 | 3 | ffnd | |
5 | simpll | |
|
6 | 3 | frnd | |
7 | df-pss | |
|
8 | 7 | baib | |
9 | 6 8 | syl | |
10 | simplr | |
|
11 | relen | |
|
12 | 11 | brrelex1i | |
13 | 5 12 | syl | |
14 | 10 13 | elmapd | |
15 | 3 14 | mpbird | |
16 | f1f1orn | |
|
17 | 16 | adantl | |
18 | f1oen3g | |
|
19 | 15 17 18 | syl2anc | |
20 | php3 | |
|
21 | 20 | ex | |
22 | 10 21 | syl | |
23 | ensdomtr | |
|
24 | 19 22 23 | syl6an | |
25 | sdomnen | |
|
26 | 24 25 | syl6 | |
27 | 9 26 | sylbird | |
28 | 27 | necon4ad | |
29 | 5 28 | mpd | |
30 | df-fo | |
|
31 | 4 29 30 | sylanbrc | |
32 | df-f1o | |
|
33 | 1 31 32 | sylanbrc | |
34 | 33 | ex | |
35 | f1of1 | |
|
36 | 34 35 | impbid1 | |