Description: Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cycpm2.c | |- C = ( toCyc ` D ) |
|
| cycpm2.d | |- ( ph -> D e. V ) |
||
| cycpm2.i | |- ( ph -> I e. D ) |
||
| cycpm2.j | |- ( ph -> J e. D ) |
||
| cycpm2.1 | |- ( ph -> I =/= J ) |
||
| cycpm2cl.s | |- S = ( SymGrp ` D ) |
||
| Assertion | cycpm2cl | |- ( ph -> ( C ` <" I J "> ) e. ( Base ` S ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cycpm2.c | |- C = ( toCyc ` D ) |
|
| 2 | cycpm2.d | |- ( ph -> D e. V ) |
|
| 3 | cycpm2.i | |- ( ph -> I e. D ) |
|
| 4 | cycpm2.j | |- ( ph -> J e. D ) |
|
| 5 | cycpm2.1 | |- ( ph -> I =/= J ) |
|
| 6 | cycpm2cl.s | |- S = ( SymGrp ` D ) |
|
| 7 | 3 4 | s2cld | |- ( ph -> <" I J "> e. Word D ) |
| 8 | 3 4 5 | s2f1 | |- ( ph -> <" I J "> : dom <" I J "> -1-1-> D ) |
| 9 | 1 2 7 8 6 | cycpmcl | |- ( ph -> ( C ` <" I J "> ) e. ( Base ` S ) ) |