Metamath Proof Explorer


Theorem mapfienlem1

Description: Lemma 1 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

Ref Expression
Hypotheses mapfien.s S=xBA|finSuppZx
mapfien.t T=xDC|finSuppWx
mapfien.w W=GZ
mapfien.f φF:C1-1 ontoA
mapfien.g φG:B1-1 ontoD
mapfien.a φAU
mapfien.b φBV
mapfien.c φCX
mapfien.d φDY
mapfien.z φZB
Assertion mapfienlem1 φfSfinSuppWGfF

Proof

Step Hyp Ref Expression
1 mapfien.s S=xBA|finSuppZx
2 mapfien.t T=xDC|finSuppWx
3 mapfien.w W=GZ
4 mapfien.f φF:C1-1 ontoA
5 mapfien.g φG:B1-1 ontoD
6 mapfien.a φAU
7 mapfien.b φBV
8 mapfien.c φCX
9 mapfien.d φDY
10 mapfien.z φZB
11 3 fvexi WV
12 11 a1i φfSWV
13 10 adantr φfSZB
14 elrabi fxBA|finSuppZxfBA
15 elmapi fBAf:AB
16 14 15 syl fxBA|finSuppZxf:AB
17 16 1 eleq2s fSf:AB
18 f1of F:C1-1 ontoAF:CA
19 4 18 syl φF:CA
20 fco f:ABF:CAfF:CB
21 17 19 20 syl2anr φfSfF:CB
22 f1of G:B1-1 ontoDG:BD
23 5 22 syl φG:BD
24 23 adantr φfSG:BD
25 ssidd φfSBB
26 8 adantr φfSCX
27 7 adantr φfSBV
28 breq1 x=ffinSuppZxfinSuppZf
29 28 1 elrab2 fSfBAfinSuppZf
30 29 simprbi fSfinSuppZf
31 30 adantl φfSfinSuppZf
32 f1of1 F:C1-1 ontoAF:C1-1A
33 4 32 syl φF:C1-1A
34 33 adantr φfSF:C1-1A
35 simpr φfSfS
36 31 34 13 35 fsuppco φfSfinSuppZfF
37 3 eqcomi GZ=W
38 37 a1i φfSGZ=W
39 12 13 21 24 25 26 27 36 38 fsuppcor φfSfinSuppWGfF