Description: An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | setcmon.c | |
|
setcmon.u | |
||
setcmon.x | |
||
setcmon.y | |
||
setciso.n | |
||
Assertion | setciso | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setcmon.c | |
|
2 | setcmon.u | |
|
3 | setcmon.x | |
|
4 | setcmon.y | |
|
5 | setciso.n | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 1 | setccat | |
9 | 2 8 | syl | |
10 | 1 2 | setcbas | |
11 | 3 10 | eleqtrd | |
12 | 4 10 | eleqtrd | |
13 | 6 7 9 11 12 5 | isoval | |
14 | 13 | eleq2d | |
15 | 6 7 9 11 12 | invfun | |
16 | funfvbrb | |
|
17 | 15 16 | syl | |
18 | 1 2 3 4 7 | setcinv | |
19 | simpl | |
|
20 | 18 19 | syl6bi | |
21 | 17 20 | sylbid | |
22 | eqid | |
|
23 | 1 2 3 4 7 | setcinv | |
24 | funrel | |
|
25 | 15 24 | syl | |
26 | releldm | |
|
27 | 26 | ex | |
28 | 25 27 | syl | |
29 | 23 28 | sylbird | |
30 | 22 29 | mpan2i | |
31 | 21 30 | impbid | |
32 | 14 31 | bitrd | |