Metamath Proof Explorer


Theorem ackbij1lem18

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

Ref Expression
Hypothesis ackbij.f F = x 𝒫 ω Fin card y x y × 𝒫 y
Assertion ackbij1lem18 A 𝒫 ω Fin b 𝒫 ω Fin F b = suc F A

Proof

Step Hyp Ref Expression
1 ackbij.f F = x 𝒫 ω Fin card y x y × 𝒫 y
2 difss A ω A A
3 1 ackbij1lem11 A 𝒫 ω Fin A ω A A A ω A 𝒫 ω Fin
4 2 3 mpan2 A 𝒫 ω Fin A ω A 𝒫 ω Fin
5 difss ω A ω
6 omsson ω On
7 5 6 sstri ω A On
8 ominf ¬ ω Fin
9 elinel2 A 𝒫 ω Fin A Fin
10 difinf ¬ ω Fin A Fin ¬ ω A Fin
11 8 9 10 sylancr A 𝒫 ω Fin ¬ ω A Fin
12 0fin Fin
13 eleq1 ω A = ω A Fin Fin
14 12 13 mpbiri ω A = ω A Fin
15 14 necon3bi ¬ ω A Fin ω A
16 11 15 syl A 𝒫 ω Fin ω A
17 onint ω A On ω 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 𝒫 ω Fin A ω A ω A 𝒫 ω Fin
23 4 21 22 syl2anc A 𝒫 ω Fin A ω A ω A 𝒫 ω Fin
24 18 eldifbd A 𝒫 ω Fin ¬ ω A A
25 disjsn A ω A = ¬ ω A A
26 24 25 sylibr A 𝒫 ω Fin A ω A =
27 ssdisj A ω A A A ω A = A ω A ω A =
28 2 26 27 sylancr A 𝒫 ω Fin A ω A ω A =
29 1 ackbij1lem9 A ω A 𝒫 ω Fin ω A 𝒫 ω Fin A ω A ω A = F A ω A ω A = F A ω A + 𝑜 F ω A
30 4 21 28 29 syl3anc A 𝒫 ω Fin F A ω A ω A = F A ω A + 𝑜 F ω A
31 1 ackbij1lem14 ω A ω F ω A = suc F ω A
32 19 31 syl A 𝒫 ω Fin F ω A = suc F ω A
33 32 oveq2d A 𝒫 ω Fin F A ω A + 𝑜 F ω A = F A ω A + 𝑜 suc F ω A
34 1 ackbij1lem10 F : 𝒫 ω Fin ω
35 34 ffvelrni A ω A 𝒫 ω Fin F A ω A ω
36 4 35 syl A 𝒫 ω Fin F A ω A ω
37 ackbij1lem3 ω A ω ω A 𝒫 ω Fin
38 19 37 syl A 𝒫 ω Fin ω A 𝒫 ω Fin
39 34 ffvelrni ω A 𝒫 ω Fin F ω A ω
40 38 39 syl A 𝒫 ω Fin F ω A ω
41 nnasuc F A ω A ω F ω A ω F A ω A + 𝑜 suc F ω A = suc F A ω A + 𝑜 F ω A
42 36 40 41 syl2anc A 𝒫 ω Fin F A ω A + 𝑜 suc F ω A = suc F A ω A + 𝑜 F ω A
43 disjdifr A ω A ω A =
44 43 a1i A 𝒫 ω Fin A ω A ω A =
45 1 ackbij1lem9 A ω A 𝒫 ω Fin ω A 𝒫 ω Fin A ω A ω A = F A ω A ω A = F A ω A + 𝑜 F ω A
46 4 38 44 45 syl3anc A 𝒫 ω Fin F A ω A ω A = F A ω A + 𝑜 F ω A
47 uncom A ω A ω A = ω A A ω A
48 onnmin ω A On a ω A ¬ a ω A
49 7 48 mpan a ω A ¬ a ω A
50 49 con2i a ω A ¬ a ω A
51 50 adantl A 𝒫 ω Fin a ω A ¬ a ω A
52 ordom Ord ω
53 ordelss Ord ω ω A ω ω A ω
54 52 19 53 sylancr A 𝒫 ω Fin ω A ω
55 54 sselda A 𝒫 ω Fin a ω A a ω
56 eldif a ω A a ω ¬ a A
57 56 simplbi2 a ω ¬ a A a ω A
58 57 orrd a ω a A a ω A
59 58 orcomd a ω a ω A a A
60 55 59 syl A 𝒫 ω Fin a ω A a ω A a A
61 orel1 ¬ a ω A a ω A a A a A
62 51 60 61 sylc A 𝒫 ω Fin a ω A a A
63 62 ex A 𝒫 ω Fin a ω A a A
64 63 ssrdv A 𝒫 ω Fin ω A A
65 undif ω A A ω A A ω A = A
66 64 65 sylib A 𝒫 ω Fin ω A A ω A = A
67 47 66 syl5eq A 𝒫 ω Fin A ω A ω A = A
68 67 fveq2d A 𝒫 ω Fin F A ω A ω A = F A
69 46 68 eqtr3d A 𝒫 ω Fin F A ω A + 𝑜 F ω A = F A
70 suceq F A ω A + 𝑜 F ω A = F A suc F A ω A + 𝑜 F ω A = suc F A
71 69 70 syl A 𝒫 ω Fin suc F A ω A + 𝑜 F ω A = suc F A
72 42 71 eqtrd A 𝒫 ω Fin F A ω A + 𝑜 suc F ω A = suc F A
73 30 33 72 3eqtrd A 𝒫 ω Fin F A ω A ω A = suc F A
74 fveqeq2 b = A ω A ω A F b = suc F A F A ω A ω A = suc F A
75 74 rspcev A ω A ω A 𝒫 ω Fin F A ω A ω A = suc F A b 𝒫 ω Fin F b = suc F A
76 23 73 75 syl2anc A 𝒫 ω Fin b 𝒫 ω Fin F b = suc F A