Metamath Proof Explorer

Theorem dprdf

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdf ⊢ G dom ⁡ DProd S → S : dom ⁡ S ⟶ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 reldmdprd ⊢ Rel ⁡ dom ⁡ DProd
2 1 brrelex2i ⊢ G dom ⁡ DProd S → S ∈ V
3 2 dmexd ⊢ G dom ⁡ DProd S → dom ⁡ S ∈ V
4 eqid ⊢ dom ⁡ S = dom ⁡ S
5 eqid ⊢ Cntz ⁡ G = Cntz ⁡ G
6 eqid ⊢ 0 G = 0 G
7 eqid ⊢ mrCls ⁡ SubGrp ⁡ G = mrCls ⁡ SubGrp ⁡ G
8 5 6 7 dmdprd ⊢ dom ⁡ S ∈ V ∧ dom ⁡ S = dom ⁡ S → G dom ⁡ DProd S ↔ G ∈ Grp ∧ S : dom ⁡ S ⟶ SubGrp ⁡ G ∧ ∀ x ∈ dom ⁡ S ∀ y ∈ dom ⁡ S ∖ x S ⁡ x ⊆ Cntz ⁡ G ⁡ S ⁡ y ∧ S ⁡ x ∩ mrCls ⁡ SubGrp ⁡ G ⁡ ⋃ S dom ⁡ S ∖ x = 0 G
9 3 4 8 sylancl ⊢ G dom ⁡ DProd S → G dom ⁡ DProd S ↔ G ∈ Grp ∧ S : dom ⁡ S ⟶ SubGrp ⁡ G ∧ ∀ x ∈ dom ⁡ S ∀ y ∈ dom ⁡ S ∖ x S ⁡ x ⊆ Cntz ⁡ G ⁡ S ⁡ y ∧ S ⁡ x ∩ mrCls ⁡ SubGrp ⁡ G ⁡ ⋃ S dom ⁡ S ∖ x = 0 G
10 9 ibi ⊢ G dom ⁡ DProd S → G ∈ Grp ∧ S : dom ⁡ S ⟶ SubGrp ⁡ G ∧ ∀ x ∈ dom ⁡ S ∀ y ∈ dom ⁡ S ∖ x S ⁡ x ⊆ Cntz ⁡ G ⁡ S ⁡ y ∧ S ⁡ x ∩ mrCls ⁡ SubGrp ⁡ G ⁡ ⋃ S dom ⁡ S ∖ x = 0 G
11 10 simp2d ⊢ G dom ⁡ DProd S → S : dom ⁡ S ⟶ SubGrp ⁡ G