This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → G dom ⁡ DProd S
dprdcntz.2 ⊢ φ → dom ⁡ S = I
Assertion dprdf2 ⊢ φ → S : I ⟶ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 dprdcntz.1 ⊢ φ → G dom ⁡ DProd S
2 dprdcntz.2 ⊢ φ → dom ⁡ S = I
3 dprdf ⊢ G dom ⁡ DProd S → S : dom ⁡ S ⟶ SubGrp ⁡ G
4 1 3 syl ⊢ φ → S : dom ⁡ S ⟶ SubGrp ⁡ G
5 2 feq2d ⊢ φ → S : dom ⁡ S ⟶ SubGrp ⁡ G ↔ S : I ⟶ SubGrp ⁡ G
6 4 5 mpbid ⊢ φ → S : I ⟶ SubGrp ⁡ G