Metamath Proof Explorer


Theorem ackbij2lem4

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypotheses ackbij.f F=x𝒫ωFincardyxy×𝒫y
ackbij.g G=xVy𝒫domxFxy
Assertion ackbij2lem4 AωBωBArecGBrecGA

Proof

Step Hyp Ref Expression
1 ackbij.f F=x𝒫ωFincardyxy×𝒫y
2 ackbij.g G=xVy𝒫domxFxy
3 fveq2 a=BrecGa=recGB
4 3 sseq2d a=BrecGBrecGarecGBrecGB
5 fveq2 a=brecGa=recGb
6 5 sseq2d a=brecGBrecGarecGBrecGb
7 fveq2 a=sucbrecGa=recGsucb
8 7 sseq2d a=sucbrecGBrecGarecGBrecGsucb
9 fveq2 a=ArecGa=recGA
10 9 sseq2d a=ArecGBrecGarecGBrecGA
11 ssidd BωrecGBrecGB
12 1 2 ackbij2lem3 bωrecGbrecGsucb
13 12 ad2antrr bωBωBbrecGbrecGsucb
14 sstr2 recGBrecGbrecGbrecGsucbrecGBrecGsucb
15 13 14 syl5com bωBωBbrecGBrecGbrecGBrecGsucb
16 4 6 8 10 11 15 findsg AωBωBArecGBrecGA