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 \to S : dom S ⟶ SubGrp (G)$

Step	Hyp	Ref	Expression
1		reldmdprd	$⊢ Rel dom DProd$
2	1	brrelex2i	$⊢ G dom DProd S \to S \in V$
3	2	dmexd	$⊢ G dom DProd S \to dom S \in 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 \in V \land dom S = dom S) \to (G dom DProd S \leftrightarrow (G \in Grp \land S : dom S ⟶ SubGrp (G) \land \forall x \in dom S (\forall y \in (dom S ∖ \{x\}) S (x) \subseteq Cntz (G) (S (y)) \land S (x) \cap mrCls (SubGrp (G)) (⋃ S [dom S ∖ \{x\}]) = \{0_{G}\})))$
9	3 4 8	sylancl	$⊢ G dom DProd S \to (G dom DProd S \leftrightarrow (G \in Grp \land S : dom S ⟶ SubGrp (G) \land \forall x \in dom S (\forall y \in (dom S ∖ \{x\}) S (x) \subseteq Cntz (G) (S (y)) \land S (x) \cap mrCls (SubGrp (G)) (⋃ S [dom S ∖ \{x\}]) = \{0_{G}\})))$
10	9	ibi	$⊢ G dom DProd S \to (G \in Grp \land S : dom S ⟶ SubGrp (G) \land \forall x \in dom S (\forall y \in (dom S ∖ \{x\}) S (x) \subseteq Cntz (G) (S (y)) \land S (x) \cap mrCls (SubGrp (G)) (⋃ S [dom S ∖ \{x\}]) = \{0_{G}\}))$
11	10	simp2d	$⊢ G dom DProd S \to S : dom S ⟶ SubGrp (G)$

Metamath Proof Explorer