Description: The predicate "is a group operation." Note that X is the base set of the group. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isgrp.1 | |
|
Assertion | isgrpo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isgrp.1 | |
|
2 | feq1 | |
|
3 | oveq | |
|
4 | oveq | |
|
5 | 4 | oveq1d | |
6 | 3 5 | eqtrd | |
7 | oveq | |
|
8 | oveq | |
|
9 | 8 | oveq2d | |
10 | 7 9 | eqtrd | |
11 | 6 10 | eqeq12d | |
12 | 11 | ralbidv | |
13 | 12 | 2ralbidv | |
14 | oveq | |
|
15 | 14 | eqeq1d | |
16 | oveq | |
|
17 | 16 | eqeq1d | |
18 | 17 | rexbidv | |
19 | 15 18 | anbi12d | |
20 | 19 | rexralbidv | |
21 | 2 13 20 | 3anbi123d | |
22 | 21 | exbidv | |
23 | df-grpo | |
|
24 | 22 23 | elab2g | |
25 | simpl | |
|
26 | 25 | ralimi | |
27 | oveq2 | |
|
28 | id | |
|
29 | 27 28 | eqeq12d | |
30 | eqcom | |
|
31 | 29 30 | bitrdi | |
32 | 31 | rspcv | |
33 | oveq2 | |
|
34 | 33 | rspceeqv | |
35 | 34 | ex | |
36 | 32 35 | syld | |
37 | 26 36 | syl5 | |
38 | 37 | reximdv | |
39 | 38 | impcom | |
40 | 39 | ralrimiva | |
41 | 40 | anim2i | |
42 | foov | |
|
43 | 41 42 | sylibr | |
44 | forn | |
|
45 | 44 | eqcomd | |
46 | 43 45 | syl | |
47 | 46 | 3adant2 | |
48 | 47 | pm4.71ri | |
49 | 48 | exbii | |
50 | 24 49 | bitrdi | |
51 | rnexg | |
|
52 | 1 | eqeq2i | |
53 | xpeq1 | |
|
54 | xpeq2 | |
|
55 | 53 54 | eqtrd | |
56 | 55 | feq2d | |
57 | feq3 | |
|
58 | 56 57 | bitrd | |
59 | raleq | |
|
60 | 59 | raleqbi1dv | |
61 | 60 | raleqbi1dv | |
62 | rexeq | |
|
63 | 62 | anbi2d | |
64 | 63 | raleqbi1dv | |
65 | 64 | rexeqbi1dv | |
66 | 58 61 65 | 3anbi123d | |
67 | 52 66 | sylbir | |
68 | 67 | ceqsexgv | |
69 | 51 68 | syl | |
70 | 50 69 | bitrd | |