Metamath Proof Explorer


Theorem dprdf2

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 ) )

Proof

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 ) )