Metamath Proof Explorer

Theorem ackbij1lem15

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 ackbij1lem15 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → ¬ F ⁡ A ∩ suc ⁡ c = F ⁡ B ∩ suc ⁡ c

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
2 simpr1 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → c ∈ ω
3 ackbij1lem3 ⊢ c ∈ ω → c ∈ 𝒫 ω ∩ Fin
4 2 3 syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → c ∈ 𝒫 ω ∩ Fin
5 simpr3 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → ¬ c ∈ B
6 ackbij1lem1 ⊢ ¬ c ∈ B → B ∩ suc ⁡ c = B ∩ c
7 5 6 syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → B ∩ suc ⁡ c = B ∩ c
8 inss2 ⊢ B ∩ c ⊆ c
9 7 8 eqsstrdi ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → B ∩ suc ⁡ c ⊆ c
10 1 ackbij1lem12 ⊢ c ∈ 𝒫 ω ∩ Fin ∧ B ∩ suc ⁡ c ⊆ c → F ⁡ B ∩ suc ⁡ c ⊆ F ⁡ c
11 4 9 10 syl2anc ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ B ∩ suc ⁡ c ⊆ F ⁡ c
12 1 ackbij1lem10 ⊢ F : 𝒫 ω ∩ Fin ⟶ ω
13 12 ffvelrni ⊢ c ∈ 𝒫 ω ∩ Fin → F ⁡ c ∈ ω
14 nnon ⊢ F ⁡ c ∈ ω → F ⁡ c ∈ On
15 onpsssuc ⊢ F ⁡ c ∈ On → F ⁡ c ⊂ suc ⁡ F ⁡ c
16 4 13 14 15 4syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c ⊂ suc ⁡ F ⁡ c
17 1 ackbij1lem14 ⊢ c ∈ ω → F ⁡ c = suc ⁡ F ⁡ c
18 2 17 syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c = suc ⁡ F ⁡ c
19 18 psseq2d ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c ⊂ F ⁡ c ↔ F ⁡ c ⊂ suc ⁡ F ⁡ c
20 16 19 mpbird ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c ⊂ F ⁡ c
21 simpll ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → A ∈ 𝒫 ω ∩ Fin
22 inss1 ⊢ A ∩ suc ⁡ c ⊆ A
23 1 ackbij1lem11 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ A ∩ suc ⁡ c ⊆ A → A ∩ suc ⁡ c ∈ 𝒫 ω ∩ Fin
24 21 22 23 sylancl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → A ∩ suc ⁡ c ∈ 𝒫 ω ∩ Fin
25 ssun1 ⊢ c ⊆ c ∪ A ∩ c
26 simpr2 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → c ∈ A
27 ackbij1lem2 ⊢ c ∈ A → A ∩ suc ⁡ c = c ∪ A ∩ c
28 26 27 syl ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → A ∩ suc ⁡ c = c ∪ A ∩ c
29 25 28 sseqtrrid ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → c ⊆ A ∩ suc ⁡ c
30 1 ackbij1lem12 ⊢ A ∩ suc ⁡ c ∈ 𝒫 ω ∩ Fin ∧ c ⊆ A ∩ suc ⁡ c → F ⁡ c ⊆ F ⁡ A ∩ suc ⁡ c
31 24 29 30 syl2anc ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c ⊆ F ⁡ A ∩ suc ⁡ c
32 20 31 psssstrd ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ c ⊂ F ⁡ A ∩ suc ⁡ c
33 11 32 sspsstrd ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ B ∩ suc ⁡ c ⊂ F ⁡ A ∩ suc ⁡ c
34 33 pssned ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ B ∩ suc ⁡ c ≠ F ⁡ A ∩ suc ⁡ c
35 34 necomd ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → F ⁡ A ∩ suc ⁡ c ≠ F ⁡ B ∩ suc ⁡ c
36 35 neneqd ⊢ A ∈ 𝒫 ω ∩ Fin ∧ B ∈ 𝒫 ω ∩ Fin ∧ c ∈ ω ∧ c ∈ A ∧ ¬ c ∈ B → ¬ F ⁡ A ∩ suc ⁡ c = F ⁡ B ∩ suc ⁡ c