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 incom ⊢ A ∖ ⋂ ω ∖ A ∩ ⋂ ω ∖ A = ⋂ ω ∖ A ∩ A ∖ ⋂ ω ∖ A
44 disjdif ⊢ ⋂ ω ∖ A ∩ A ∖ ⋂ ω ∖ A = ∅
45 43 44 eqtri ⊢ A ∖ ⋂ ω ∖ A ∩ ⋂ ω ∖ A = ∅
46 45 a1i ⊢ A ∈ 𝒫 ω ∩ Fin → A ∖ ⋂ ω ∖ A ∩ ⋂ ω ∖ A = ∅
47 1 ackbij1lem9 ⊢ A ∖ ⋂ ω ∖ A ∈ 𝒫 ω ∩ Fin ∧ ⋂ ω ∖ A ∈ 𝒫 ω ∩ Fin ∧ A ∖ ⋂ ω ∖ A ∩ ⋂ ω ∖ A = ∅ → F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A
48 4 38 46 47 syl3anc ⊢ A ∈ 𝒫 ω ∩ Fin → F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A
49 uncom ⊢ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = ⋂ ω ∖ A ∪ A ∖ ⋂ ω ∖ A
50 onnmin ⊢ ω ∖ A ⊆ On ∧ a ∈ ω ∖ A → ¬ a ∈ ⋂ ω ∖ A
51 7 50 mpan ⊢ a ∈ ω ∖ A → ¬ a ∈ ⋂ ω ∖ A
52 51 con2i ⊢ a ∈ ⋂ ω ∖ A → ¬ a ∈ ω ∖ A
53 52 adantl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ a ∈ ⋂ ω ∖ A → ¬ a ∈ ω ∖ A
54 ordom ⊢ Ord ⁡ ω
55 ordelss ⊢ Ord ⁡ ω ∧ ⋂ ω ∖ A ∈ ω → ⋂ ω ∖ A ⊆ ω
56 54 19 55 sylancr ⊢ A ∈ 𝒫 ω ∩ Fin → ⋂ ω ∖ A ⊆ ω
57 56 sselda ⊢ A ∈ 𝒫 ω ∩ Fin ∧ a ∈ ⋂ ω ∖ A → a ∈ ω
58 eldif ⊢ a ∈ ω ∖ A ↔ a ∈ ω ∧ ¬ a ∈ A
59 58 simplbi2 ⊢ a ∈ ω → ¬ a ∈ A → a ∈ ω ∖ A
60 59 orrd ⊢ a ∈ ω → a ∈ A ∨ a ∈ ω ∖ A
61 60 orcomd ⊢ a ∈ ω → a ∈ ω ∖ A ∨ a ∈ A
62 57 61 syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ a ∈ ⋂ ω ∖ A → a ∈ ω ∖ A ∨ a ∈ A
63 orel1 ⊢ ¬ a ∈ ω ∖ A → a ∈ ω ∖ A ∨ a ∈ A → a ∈ A
64 53 62 63 sylc ⊢ A ∈ 𝒫 ω ∩ Fin ∧ a ∈ ⋂ ω ∖ A → a ∈ A
65 64 ex ⊢ A ∈ 𝒫 ω ∩ Fin → a ∈ ⋂ ω ∖ A → a ∈ A
66 65 ssrdv ⊢ A ∈ 𝒫 ω ∩ Fin → ⋂ ω ∖ A ⊆ A
67 undif ⊢ ⋂ ω ∖ A ⊆ A ↔ ⋂ ω ∖ A ∪ A ∖ ⋂ ω ∖ A = A
68 66 67 sylib ⊢ A ∈ 𝒫 ω ∩ Fin → ⋂ ω ∖ A ∪ A ∖ ⋂ ω ∖ A = A
69 49 68 syl5eq ⊢ A ∈ 𝒫 ω ∩ Fin → A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = A
70 69 fveq2d ⊢ A ∈ 𝒫 ω ∩ Fin → F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = F ⁡ A
71 48 70 eqtr3d ⊢ A ∈ 𝒫 ω ∩ Fin → F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A = F ⁡ A
72 suceq ⊢ F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A = F ⁡ A → suc ⁡ F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A = suc ⁡ F ⁡ A
73 71 72 syl ⊢ A ∈ 𝒫 ω ∩ Fin → suc ⁡ F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 F ⁡ ⋂ ω ∖ A = suc ⁡ F ⁡ A
74 42 73 eqtrd ⊢ A ∈ 𝒫 ω ∩ Fin → F ⁡ A ∖ ⋂ ω ∖ A + 𝑜 suc ⁡ F ⁡ ⋂ ω ∖ A = suc ⁡ F ⁡ A
75 30 33 74 3eqtrd ⊢ A ∈ 𝒫 ω ∩ Fin → F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = suc ⁡ F ⁡ A
76 fveqeq2 ⊢ b = A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A → F ⁡ b = suc ⁡ F ⁡ A ↔ F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = suc ⁡ F ⁡ A
77 76 rspcev ⊢ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A ∈ 𝒫 ω ∩ Fin ∧ F ⁡ A ∖ ⋂ ω ∖ A ∪ ⋂ ω ∖ A = suc ⁡ F ⁡ A → ∃ b ∈ 𝒫 ω ∩ Fin F ⁡ b = suc ⁡ F ⁡ A
78 23 75 77 syl2anc ⊢ A ∈ 𝒫 ω ∩ Fin → ∃ b ∈ 𝒫 ω ∩ Fin F ⁡ b = suc ⁡ F ⁡ A