Metamath Proof Explorer


Theorem imasaddflem

Description: The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f φF:VontoB
imasaddf.e φaVbVpVqVFa=FpFb=FqFa·˙b=Fp·˙q
imasaddflem.a φ˙=pVqVFpFqFp·˙q
imasaddflem.c φpVqVp·˙qV
Assertion imasaddflem φ˙:B×BB

Proof

Step Hyp Ref Expression
1 imasaddf.f φF:VontoB
2 imasaddf.e φaVbVpVqVFa=FpFb=FqFa·˙b=Fp·˙q
3 imasaddflem.a φ˙=pVqVFpFqFp·˙q
4 imasaddflem.c φpVqVp·˙qV
5 1 2 3 imasaddfnlem φ˙FnB×B
6 fof F:VontoBF:VB
7 1 6 syl φF:VB
8 ffvelrn F:VBpVFpB
9 ffvelrn F:VBqVFqB
10 8 9 anim12dan F:VBpVqVFpBFqB
11 opelxpi FpBFqBFpFqB×B
12 10 11 syl F:VBpVqVFpFqB×B
13 7 12 sylan φpVqVFpFqB×B
14 ffvelrn F:VBp·˙qVFp·˙qB
15 7 4 14 syl2an2r φpVqVFp·˙qB
16 13 15 opelxpd φpVqVFpFqFp·˙qB×B×B
17 16 snssd φpVqVFpFqFp·˙qB×B×B
18 17 anassrs φpVqVFpFqFp·˙qB×B×B
19 18 iunssd φpVqVFpFqFp·˙qB×B×B
20 19 iunssd φpVqVFpFqFp·˙qB×B×B
21 3 20 eqsstrd φ˙B×B×B
22 dff2 ˙:B×BB˙FnB×B˙B×B×B
23 5 21 22 sylanbrc φ˙:B×BB