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