Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eqgval.x | |
|
eqgval.n | |
||
eqgval.p | |
||
eqgval.r | |
||
Assertion | eqgfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqgval.x | |
|
2 | eqgval.n | |
|
3 | eqgval.p | |
|
4 | eqgval.r | |
|
5 | elex | |
|
6 | 1 | fvexi | |
7 | 6 | ssex | |
8 | simpl | |
|
9 | 8 | fveq2d | |
10 | 9 1 | eqtr4di | |
11 | 10 | sseq2d | |
12 | 8 | fveq2d | |
13 | 12 3 | eqtr4di | |
14 | 8 | fveq2d | |
15 | 14 2 | eqtr4di | |
16 | 15 | fveq1d | |
17 | eqidd | |
|
18 | 13 16 17 | oveq123d | |
19 | simpr | |
|
20 | 18 19 | eleq12d | |
21 | 11 20 | anbi12d | |
22 | 21 | opabbidv | |
23 | df-eqg | |
|
24 | 6 6 | xpex | |
25 | simpl | |
|
26 | vex | |
|
27 | vex | |
|
28 | 26 27 | prss | |
29 | 25 28 | sylibr | |
30 | 29 | ssopab2i | |
31 | df-xp | |
|
32 | 30 31 | sseqtrri | |
33 | 24 32 | ssexi | |
34 | 22 23 33 | ovmpoa | |
35 | 4 34 | eqtrid | |
36 | 5 7 35 | syl2an | |