Theorem dprdf

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

	Ref	Expression
Assertion	dprdf	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		reldmdprd	⊢ Rel dom DProd
2	1	brrelex2i	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
3	2	dmexd	⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
4		eqid	⊢ dom 𝑆 = dom 𝑆
5		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7		eqid	⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
8	5 6 7	dmdprd	⊢ ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
9	3 4 8	sylancl	⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
10	9	ibi	⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) )
11	10	simp2d	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) )