Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dprdcntz.1 | |- ( ph -> G dom DProd S ) |
|
dprdcntz.2 | |- ( ph -> dom S = I ) |
||
Assertion | dprdf2 | |- ( ph -> S : I --> ( SubGrp ` G ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dprdcntz.1 | |- ( ph -> G dom DProd S ) |
|
2 | dprdcntz.2 | |- ( ph -> dom S = I ) |
|
3 | dprdf | |- ( G dom DProd S -> S : dom S --> ( SubGrp ` G ) ) |
|
4 | 1 3 | syl | |- ( ph -> S : dom S --> ( SubGrp ` G ) ) |
5 | 2 | feq2d | |- ( ph -> ( S : dom S --> ( SubGrp ` G ) <-> S : I --> ( SubGrp ` G ) ) ) |
6 | 4 5 | mpbid | |- ( ph -> S : I --> ( SubGrp ` G ) ) |