Metamath Proof Explorer


Theorem ackbij1lem18

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

Ref Expression
Hypothesis ackbij.f F=x𝒫ωFincardyxy×𝒫y
Assertion ackbij1lem18 A𝒫ωFinb𝒫ωFinFb=sucFA

Proof

Step Hyp Ref Expression
1 ackbij.f F=x𝒫ωFincardyxy×𝒫y
2 difss AωAA
3 1 ackbij1lem11 A𝒫ωFinAωAAAωA𝒫ωFin
4 2 3 mpan2 A𝒫ωFinAωA𝒫ωFin
5 difss ωAω
6 omsson ωOn
7 5 6 sstri ωAOn
8 ominf ¬ωFin
9 elinel2 A𝒫ωFinAFin
10 difinf ¬ωFinAFin¬ωAFin
11 8 9 10 sylancr A𝒫ωFin¬ωAFin
12 0fin Fin
13 eleq1 ωA=ωAFinFin
14 12 13 mpbiri ωA=ωAFin
15 14 necon3bi ¬ωAFinωA
16 11 15 syl A𝒫ωFinωA
17 onint ωAOnωAωAωA
18 7 16 17 sylancr A𝒫ωFinωAωA
19 18 eldifad A𝒫ωFinωAω
20 ackbij1lem4 ωAωωA𝒫ωFin
21 19 20 syl A𝒫ωFinωA𝒫ωFin
22 ackbij1lem6 AωA𝒫ωFinωA𝒫ωFinAωAωA𝒫ωFin
23 4 21 22 syl2anc A𝒫ωFinAωAωA𝒫ωFin
24 18 eldifbd A𝒫ωFin¬ωAA
25 disjsn AωA=¬ωAA
26 24 25 sylibr A𝒫ωFinAωA=
27 ssdisj AωAAAωA=AωAωA=
28 2 26 27 sylancr A𝒫ωFinAωAωA=
29 1 ackbij1lem9 AωA𝒫ωFinωA𝒫ωFinAωAωA=FAωAωA=FAωA+𝑜FωA
30 4 21 28 29 syl3anc A𝒫ωFinFAωAωA=FAωA+𝑜FωA
31 1 ackbij1lem14 ωAωFωA=sucFωA
32 19 31 syl A𝒫ωFinFωA=sucFωA
33 32 oveq2d A𝒫ωFinFAωA+𝑜FωA=FAωA+𝑜sucFωA
34 1 ackbij1lem10 F:𝒫ωFinω
35 34 ffvelrni AωA𝒫ωFinFAωAω
36 4 35 syl A𝒫ωFinFAωAω
37 ackbij1lem3 ωAωωA𝒫ωFin
38 19 37 syl A𝒫ωFinωA𝒫ωFin
39 34 ffvelrni ωA𝒫ωFinFωAω
40 38 39 syl A𝒫ωFinFωAω
41 nnasuc FAωAωFωAωFAωA+𝑜sucFωA=sucFAωA+𝑜FωA
42 36 40 41 syl2anc A𝒫ωFinFAωA+𝑜sucFωA=sucFAωA+𝑜FωA
43 disjdifr AωAωA=
44 43 a1i A𝒫ωFinAωAωA=
45 1 ackbij1lem9 AωA𝒫ωFinωA𝒫ωFinAωAωA=FAωAωA=FAωA+𝑜FωA
46 4 38 44 45 syl3anc A𝒫ωFinFAωAωA=FAωA+𝑜FωA
47 uncom AωAωA=ωAAωA
48 onnmin ωAOnaωA¬aωA
49 7 48 mpan aωA¬aωA
50 49 con2i aωA¬aωA
51 50 adantl A𝒫ωFinaωA¬aωA
52 ordom Ordω
53 ordelss OrdωωAωωAω
54 52 19 53 sylancr A𝒫ωFinωAω
55 54 sselda A𝒫ωFinaωAaω
56 eldif aωAaω¬aA
57 56 simplbi2 aω¬aAaωA
58 57 orrd aωaAaωA
59 58 orcomd aωaωAaA
60 55 59 syl A𝒫ωFinaωAaωAaA
61 orel1 ¬aωAaωAaAaA
62 51 60 61 sylc A𝒫ωFinaωAaA
63 62 ex A𝒫ωFinaωAaA
64 63 ssrdv A𝒫ωFinωAA
65 undif ωAAωAAωA=A
66 64 65 sylib A𝒫ωFinωAAωA=A
67 47 66 eqtrid A𝒫ωFinAωAωA=A
68 67 fveq2d A𝒫ωFinFAωAωA=FA
69 46 68 eqtr3d A𝒫ωFinFAωA+𝑜FωA=FA
70 suceq FAωA+𝑜FωA=FAsucFAωA+𝑜FωA=sucFA
71 69 70 syl A𝒫ωFinsucFAωA+𝑜FωA=sucFA
72 42 71 eqtrd A𝒫ωFinFAωA+𝑜sucFωA=sucFA
73 30 33 72 3eqtrd A𝒫ωFinFAωAωA=sucFA
74 fveqeq2 b=AωAωAFb=sucFAFAωAωA=sucFA
75 74 rspcev AωAωA𝒫ωFinFAωAωA=sucFAb𝒫ωFinFb=sucFA
76 23 73 75 syl2anc A𝒫ωFinb𝒫ωFinFb=sucFA