Metamath Proof Explorer


Theorem dprddisj

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

Ref Expression
Hypotheses dprdcntz.1 φGdomDProdS
dprdcntz.2 φdomS=I
dprdcntz.3 φXI
dprddisj.0 0˙=0G
dprddisj.k K=mrClsSubGrpG
Assertion dprddisj φSXKSIX=0˙

Proof

Step Hyp Ref Expression
1 dprdcntz.1 φGdomDProdS
2 dprdcntz.2 φdomS=I
3 dprdcntz.3 φXI
4 dprddisj.0 0˙=0G
5 dprddisj.k K=mrClsSubGrpG
6 fveq2 x=XSx=SX
7 sneq x=Xx=X
8 7 difeq2d x=XIx=IX
9 8 imaeq2d x=XSIx=SIX
10 9 unieqd x=XSIx=SIX
11 10 fveq2d x=XKSIx=KSIX
12 6 11 ineq12d x=XSxKSIx=SXKSIX
13 12 eqeq1d x=XSxKSIx=0˙SXKSIX=0˙
14 1 2 dprddomcld φIV
15 eqid CntzG=CntzG
16 15 4 5 dmdprd IVdomS=IGdomDProdSGGrpS:ISubGrpGxIyIxSxCntzGSySxKSIx=0˙
17 14 2 16 syl2anc φGdomDProdSGGrpS:ISubGrpGxIyIxSxCntzGSySxKSIx=0˙
18 1 17 mpbid φGGrpS:ISubGrpGxIyIxSxCntzGSySxKSIx=0˙
19 18 simp3d φxIyIxSxCntzGSySxKSIx=0˙
20 simpr yIxSxCntzGSySxKSIx=0˙SxKSIx=0˙
21 20 ralimi xIyIxSxCntzGSySxKSIx=0˙xISxKSIx=0˙
22 19 21 syl φxISxKSIx=0˙
23 13 22 3 rspcdva φSXKSIX=0˙