Metamath Proof Explorer


Theorem ackbij1lem14

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

Ref Expression
Hypothesis ackbij.f F=x𝒫ωFincardyxy×𝒫y
Assertion ackbij1lem14 AωFA=sucFA

Proof

Step Hyp Ref Expression
1 ackbij.f F=x𝒫ωFincardyxy×𝒫y
2 1 ackbij1lem8 AωFA=card𝒫A
3 pweq a=𝒫a=𝒫
4 3 fveq2d a=card𝒫a=card𝒫
5 fveq2 a=Fa=F
6 suceq Fa=FsucFa=sucF
7 5 6 syl a=sucFa=sucF
8 4 7 eqeq12d a=card𝒫a=sucFacard𝒫=sucF
9 pweq a=b𝒫a=𝒫b
10 9 fveq2d a=bcard𝒫a=card𝒫b
11 fveq2 a=bFa=Fb
12 suceq Fa=FbsucFa=sucFb
13 11 12 syl a=bsucFa=sucFb
14 10 13 eqeq12d a=bcard𝒫a=sucFacard𝒫b=sucFb
15 pweq a=sucb𝒫a=𝒫sucb
16 15 fveq2d a=sucbcard𝒫a=card𝒫sucb
17 fveq2 a=sucbFa=Fsucb
18 suceq Fa=FsucbsucFa=sucFsucb
19 17 18 syl a=sucbsucFa=sucFsucb
20 16 19 eqeq12d a=sucbcard𝒫a=sucFacard𝒫sucb=sucFsucb
21 pweq a=A𝒫a=𝒫A
22 21 fveq2d a=Acard𝒫a=card𝒫A
23 fveq2 a=AFa=FA
24 suceq Fa=FAsucFa=sucFA
25 23 24 syl a=AsucFa=sucFA
26 22 25 eqeq12d a=Acard𝒫a=sucFacard𝒫A=sucFA
27 df-1o 1𝑜=suc
28 pw0 𝒫=
29 28 fveq2i card𝒫=card
30 0ex V
31 cardsn Vcard=1𝑜
32 30 31 ax-mp card=1𝑜
33 29 32 eqtri card𝒫=1𝑜
34 1 ackbij1lem13 F=
35 suceq F=sucF=suc
36 34 35 ax-mp sucF=suc
37 27 33 36 3eqtr4i card𝒫=sucF
38 oveq2 card𝒫b=sucFbcard𝒫b+𝑜card𝒫b=card𝒫b+𝑜sucFb
39 38 adantl bωcard𝒫b=sucFbcard𝒫b+𝑜card𝒫b=card𝒫b+𝑜sucFb
40 ackbij1lem5 bωcard𝒫sucb=card𝒫b+𝑜card𝒫b
41 40 adantr bωcard𝒫b=sucFbcard𝒫sucb=card𝒫b+𝑜card𝒫b
42 df-suc sucb=bb
43 42 equncomi sucb=bb
44 43 fveq2i Fsucb=Fbb
45 ackbij1lem4 bωb𝒫ωFin
46 45 adantr bωcard𝒫b=sucFbb𝒫ωFin
47 ackbij1lem3 bωb𝒫ωFin
48 47 adantr bωcard𝒫b=sucFbb𝒫ωFin
49 incom bb=bb
50 nnord bωOrdb
51 orddisj Ordbbb=
52 50 51 syl bωbb=
53 49 52 eqtrid bωbb=
54 53 adantr bωcard𝒫b=sucFbbb=
55 1 ackbij1lem9 b𝒫ωFinb𝒫ωFinbb=Fbb=Fb+𝑜Fb
56 46 48 54 55 syl3anc bωcard𝒫b=sucFbFbb=Fb+𝑜Fb
57 1 ackbij1lem8 bωFb=card𝒫b
58 57 adantr bωcard𝒫b=sucFbFb=card𝒫b
59 58 oveq1d bωcard𝒫b=sucFbFb+𝑜Fb=card𝒫b+𝑜Fb
60 56 59 eqtrd bωcard𝒫b=sucFbFbb=card𝒫b+𝑜Fb
61 44 60 eqtrid bωcard𝒫b=sucFbFsucb=card𝒫b+𝑜Fb
62 suceq Fsucb=card𝒫b+𝑜FbsucFsucb=succard𝒫b+𝑜Fb
63 61 62 syl bωcard𝒫b=sucFbsucFsucb=succard𝒫b+𝑜Fb
64 nnfi bωbFin
65 pwfi bFin𝒫bFin
66 64 65 sylib bω𝒫bFin
67 66 adantr bωcard𝒫b=sucFb𝒫bFin
68 ficardom 𝒫bFincard𝒫bω
69 67 68 syl bωcard𝒫b=sucFbcard𝒫bω
70 1 ackbij1lem10 F:𝒫ωFinω
71 70 ffvelrni b𝒫ωFinFbω
72 48 71 syl bωcard𝒫b=sucFbFbω
73 nnasuc card𝒫bωFbωcard𝒫b+𝑜sucFb=succard𝒫b+𝑜Fb
74 69 72 73 syl2anc bωcard𝒫b=sucFbcard𝒫b+𝑜sucFb=succard𝒫b+𝑜Fb
75 63 74 eqtr4d bωcard𝒫b=sucFbsucFsucb=card𝒫b+𝑜sucFb
76 39 41 75 3eqtr4d bωcard𝒫b=sucFbcard𝒫sucb=sucFsucb
77 76 ex bωcard𝒫b=sucFbcard𝒫sucb=sucFsucb
78 8 14 20 26 37 77 finds Aωcard𝒫A=sucFA
79 2 78 eqtrd AωFA=sucFA