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 0fi ⊢ ∅ ∈ 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 ffvelcdmi ⊢ 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 ffvelcdmi ⊢ ⋂ ω ∖ 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 eqtrid ⊢ 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