Description: The range of a group operation. Useful for satisfying group base set hypotheses of the form X = ran G . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grprn.1 | |
|
grprn.2 | |
||
Assertion | grporn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grprn.1 | |
|
2 | grprn.2 | |
|
3 | eqid | |
|
4 | 3 | grpofo | |
5 | fofun | |
|
6 | 1 4 5 | mp2b | |
7 | df-fn | |
|
8 | 6 2 7 | mpbir2an | |
9 | fofn | |
|
10 | 1 4 9 | mp2b | |
11 | fndmu | |
|
12 | xpid11 | |
|
13 | 11 12 | sylib | |
14 | 8 10 13 | mp2an | |