Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efgval.w | |
|
efgval.r | |
||
Assertion | efgval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efgval.w | |
|
2 | efgval.r | |
|
3 | vex | |
|
4 | 2on | |
|
5 | 4 | elexi | |
6 | 3 5 | xpex | |
7 | wrdexg | |
|
8 | fvi | |
|
9 | 6 7 8 | mp2b | |
10 | xpeq1 | |
|
11 | wrdeq | |
|
12 | 10 11 | syl | |
13 | 12 | fveq2d | |
14 | 9 13 | eqtr3id | |
15 | 14 1 | eqtr4di | |
16 | ereq2 | |
|
17 | 15 16 | syl | |
18 | raleq | |
|
19 | 18 | ralbidv | |
20 | 15 19 | raleqbidv | |
21 | 17 20 | anbi12d | |
22 | 21 | abbidv | |
23 | 22 | inteqd | |
24 | df-efg | |
|
25 | 1 | efglem | |
26 | intexab | |
|
27 | 25 26 | mpbi | |
28 | 23 24 27 | fvmpt | |
29 | fvprc | |
|
30 | abn0 | |
|
31 | 25 30 | mpbir | |
32 | intssuni | |
|
33 | 31 32 | ax-mp | |
34 | erssxp | |
|
35 | 1 | efgrcl | |
36 | 35 | simpld | |
37 | 36 | con3i | |
38 | 37 | eq0rdv | |
39 | 38 | xpeq2d | |
40 | xp0 | |
|
41 | 39 40 | eqtrdi | |
42 | ss0b | |
|
43 | 41 42 | sylibr | |
44 | 34 43 | sylan9ssr | |
45 | 44 | ex | |
46 | 45 | adantrd | |
47 | 46 | alrimiv | |
48 | sseq1 | |
|
49 | 48 | ralab2 | |
50 | 47 49 | sylibr | |
51 | unissb | |
|
52 | 50 51 | sylibr | |
53 | 33 52 | sstrid | |
54 | ss0 | |
|
55 | 53 54 | syl | |
56 | 29 55 | eqtr4d | |
57 | 28 56 | pm2.61i | |
58 | 2 57 | eqtri | |