Metamath Proof Explorer

Theorem incexclem

Description: Lemma for incexc . (Contributed by Mario Carneiro, 7-Aug-2017)

Ref Expression
Assertion incexclem ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
2 uni0 ⊢ ∪ ∅ = ∅
3 1 2 eqtrdi ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∅ )
4 3 ineq2d ⊢ ( 𝑥 = ∅ → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ∅ ) )
5 in0 ⊢ ( 𝑏 ∩ ∅ ) = ∅
6 4 5 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑏 ∩ ∪ 𝑥 ) = ∅ )
7 6 fveq2d ⊢ ( 𝑥 = ∅ → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ∅ ) )
8 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
9 7 8 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = 0 )
10 9 oveq2d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − 0 ) )
11 pweq ⊢ ( 𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅ )
12 pw0 ⊢ 𝒫 ∅ = { ∅ }
13 11 12 eqtrdi ⊢ ( 𝑥 = ∅ → 𝒫 𝑥 = { ∅ } )
14 13 sumeq1d ⊢ ( 𝑥 = ∅ → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
15 10 14 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
16 15 ralbidv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
17 unieq ⊢ ( 𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦 )
18 17 ineq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ∪ 𝑦 ) )
19 18 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) )
20 19 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) )
21 pweq ⊢ ( 𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦 )
22 21 sumeq1d ⊢ ( 𝑥 = 𝑦 → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
23 20 22 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
24 23 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
25 unieq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑥 = ∪ ( 𝑦 ∪ { 𝑧 } ) )
26 uniun ⊢ ∪ ( 𝑦 ∪ { 𝑧 } ) = ( ∪ 𝑦 ∪ ∪ { 𝑧 } )
27 vex ⊢ 𝑧 ∈ V
28 27 unisn ⊢ ∪ { 𝑧 } = 𝑧
29 28 uneq2i ⊢ ( ∪ 𝑦 ∪ ∪ { 𝑧 } ) = ( ∪ 𝑦 ∪ 𝑧 )
30 26 29 eqtri ⊢ ∪ ( 𝑦 ∪ { 𝑧 } ) = ( ∪ 𝑦 ∪ 𝑧 )
31 25 30 eqtrdi ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑥 = ( ∪ 𝑦 ∪ 𝑧 ) )
32 31 ineq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) )
33 32 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) )
34 33 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) )
35 pweq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → 𝒫 𝑥 = 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
36 35 sumeq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
37 34 36 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
38 37 ralbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
39 unieq ⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
40 39 ineq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ∪ 𝐴 ) )
41 40 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) )
42 41 oveq2d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) )
43 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
44 43 sumeq1d ⊢ ( 𝑥 = 𝐴 → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
45 42 44 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
46 45 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
47 hashcl ⊢ ( 𝑏 ∈ Fin → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
48 47 nn0cnd ⊢ ( 𝑏 ∈ Fin → ( ♯ ‘ 𝑏 ) ∈ ℂ )
49 48 mulid2d ⊢ ( 𝑏 ∈ Fin → ( 1 · ( ♯ ‘ 𝑏 ) ) = ( ♯ ‘ 𝑏 ) )
50 0ex ⊢ ∅ ∈ V
51 49 48 eqeltrd ⊢ ( 𝑏 ∈ Fin → ( 1 · ( ♯ ‘ 𝑏 ) ) ∈ ℂ )
52 fveq2 ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ∅ ) )
53 52 8 eqtrdi ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = 0 )
54 53 oveq2d ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( - 1 ↑ 0 ) )
55 neg1cn ⊢ - 1 ∈ ℂ
56 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
57 55 56 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
58 54 57 eqtrdi ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = 1 )
59 rint0 ⊢ ( 𝑠 = ∅ → ( 𝑏 ∩ ∩ 𝑠 ) = 𝑏 )
60 59 fveq2d ⊢ ( 𝑠 = ∅ → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ 𝑏 ) )
61 58 60 oveq12d ⊢ ( 𝑠 = ∅ → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
62 61 sumsn ⊢ ( ( ∅ ∈ V ∧ ( 1 · ( ♯ ‘ 𝑏 ) ) ∈ ℂ ) → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
63 50 51 62 sylancr ⊢ ( 𝑏 ∈ Fin → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
64 48 subid1d ⊢ ( 𝑏 ∈ Fin → ( ( ♯ ‘ 𝑏 ) − 0 ) = ( ♯ ‘ 𝑏 ) )
65 49 63 64 3eqtr4rd ⊢ ( 𝑏 ∈ Fin → ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
66 65 rgen ⊢ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) )
67 fveq2 ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ 𝑥 ) )
68 ineq1 ⊢ ( 𝑏 = 𝑥 → ( 𝑏 ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ∪ 𝑦 ) )
69 68 fveq2d ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) = ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) )
70 67 69 oveq12d ⊢ ( 𝑏 = 𝑥 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) )
71 simpl ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑏 = 𝑥 )
72 71 ineq1d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ∩ 𝑠 ) )
73 72 fveq2d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) )
74 73 oveq2d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
75 74 sumeq2dv ⊢ ( 𝑏 = 𝑥 → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
76 70 75 eqeq12d ⊢ ( 𝑏 = 𝑥 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
77 76 rspcva ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
78 77 adantll ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
79 simpr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝑥 ∈ Fin )
80 inss1 ⊢ ( 𝑥 ∩ 𝑧 ) ⊆ 𝑥
81 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝑧 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑧 ) ∈ Fin )
82 79 80 81 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ 𝑧 ) ∈ Fin )
83 fveq2 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) )
84 ineq1 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∪ 𝑦 ) = ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) )
85 in32 ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ 𝑧 )
86 inass ⊢ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ 𝑧 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) )
87 85 86 eqtri ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) )
88 84 87 eqtrdi ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) )
89 88 fveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) )
90 83 89 oveq12d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) )
91 ineq1 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) )
92 in32 ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) = ( ( 𝑥 ∩ ∩ 𝑠 ) ∩ 𝑧 )
93 inass ⊢ ( ( 𝑥 ∩ ∩ 𝑠 ) ∩ 𝑧 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) )
94 92 93 eqtri ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) )
95 91 94 eqtrdi ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) )
96 95 fveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) )
97 96 oveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
98 97 sumeq2sdv ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
99 90 98 eqeq12d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
100 99 rspcva ⊢ ( ( ( 𝑥 ∩ 𝑧 ) ∈ Fin ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
101 82 100 sylan ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
102 78 101 oveq12d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
103 inss1 ⊢ ( 𝑥 ∩ ∪ 𝑦 ) ⊆ 𝑥
104 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ∪ 𝑦 ) ⊆ 𝑥 ) → ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin )
105 79 103 104 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin )
106 hashcl ⊢ ( ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℕ0 )
107 105 106 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℕ0 )
108 107 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℂ )
109 hashcl ⊢ ( ( 𝑥 ∩ 𝑧 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℕ0 )
110 82 109 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℕ0 )
111 110 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℂ )
112 inss1 ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ⊆ 𝑥
113 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ⊆ 𝑥 ) → ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin )
114 79 112 113 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin )
115 hashcl ⊢ ( ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℕ0 )
116 114 115 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℕ0 )
117 116 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℂ )
118 hashun3 ⊢ ( ( ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin ∧ ( 𝑥 ∩ 𝑧 ) ∈ Fin ) → ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) ) )
119 105 82 118 syl2anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) ) )
120 indi ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) )
121 120 fveq2i ⊢ ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) )
122 inindi ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) )
123 122 fveq2i ⊢ ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) = ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) )
124 123 oveq2i ⊢ ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) )
125 119 121 124 3eqtr4g ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) )
126 108 111 117 125 assraddsubd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
127 126 oveq2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) ) )
128 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
129 128 adantl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
130 129 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ 𝑥 ) ∈ ℂ )
131 111 117 subcld ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ∈ ℂ )
132 130 108 131 subsub4d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) ) )
133 127 132 eqtr4d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
134 133 adantr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
135 disjdif ⊢ ( 𝒫 𝑦 ∩ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = ∅
136 135 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝒫 𝑦 ∩ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = ∅ )
137 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
138 137 sspwi ⊢ 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } )
139 undif ⊢ ( 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
140 138 139 mpbi ⊢ ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = 𝒫 ( 𝑦 ∪ { 𝑧 } )
141 140 eqcomi ⊢ 𝒫 ( 𝑦 ∪ { 𝑧 } ) = ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) )
142 141 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 ( 𝑦 ∪ { 𝑧 } ) = ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) )
143 simpll ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝑦 ∈ Fin )
144 snfi ⊢ { 𝑧 } ∈ Fin
145 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
146 143 144 145 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
147 pwfi ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ↔ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
148 146 147 sylib ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
149 55 a1i ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → - 1 ∈ ℂ )
150 elpwi ⊢ ( 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) → 𝑠 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
151 ssfi ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 𝑠 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑠 ∈ Fin )
152 146 150 151 syl2an ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → 𝑠 ∈ Fin )
153 hashcl ⊢ ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
154 152 153 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
155 149 154 expcld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
156 simplr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → 𝑥 ∈ Fin )
157 inss1 ⊢ ( 𝑥 ∩ ∩ 𝑠 ) ⊆ 𝑥
158 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ∩ 𝑠 ) ⊆ 𝑥 ) → ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin )
159 156 157 158 sylancl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin )
160 hashcl ⊢ ( ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
161 159 160 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
162 161 nn0cnd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℂ )
163 155 162 mulcld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
164 136 142 148 163 fsumsplit ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
165 fveq2 ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) )
166 165 oveq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) )
167 inteq ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ∩ 𝑠 = ∩ ( 𝑡 ∪ { 𝑧 } ) )
168 27 intunsn ⊢ ∩ ( 𝑡 ∪ { 𝑧 } ) = ( ∩ 𝑡 ∩ 𝑧 )
169 167 168 eqtrdi ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ∩ 𝑠 = ( ∩ 𝑡 ∩ 𝑧 ) )
170 169 ineq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( 𝑥 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) )
171 170 fveq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) )
172 166 171 oveq12d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) )
173 pwfi ⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin )
174 143 173 sylib ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 𝑦 ∈ Fin )
175 eqid ⊢ ( 𝑢 ∈ 𝒫 𝑦 ↦ ( 𝑢 ∪ { 𝑧 } ) ) = ( 𝑢 ∈ 𝒫 𝑦 ↦ ( 𝑢 ∪ { 𝑧 } ) )
176 elpwi ⊢ ( 𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦 )
177 176 adantl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → 𝑢 ⊆ 𝑦 )
178 unss1 ⊢ ( 𝑢 ⊆ 𝑦 → ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
179 177 178 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
180 vex ⊢ 𝑢 ∈ V
181 snex ⊢ { 𝑧 } ∈ V
182 180 181 unex ⊢ ( 𝑢 ∪ { 𝑧 } ) ∈ V
183 182 elpw ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
184 179 183 sylibr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
185 simpllr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
186 elpwi ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 𝑦 → ( 𝑢 ∪ { 𝑧 } ) ⊆ 𝑦 )
187 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑢 ∪ { 𝑧 } )
188 27 snss ⊢ ( 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) ↔ { 𝑧 } ⊆ ( 𝑢 ∪ { 𝑧 } ) )
189 187 188 mpbir ⊢ 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } )
190 189 a1i ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) )
191 ssel ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ⊆ 𝑦 → ( 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) → 𝑧 ∈ 𝑦 ) )
192 186 190 191 syl2imc ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦 ) )
193 185 192 mtod ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ¬ ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 𝑦 )
194 184 193 eldifd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ( 𝑢 ∪ { 𝑧 } ) ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) )
195 eldifi ⊢ ( 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
196 195 adantl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
197 196 elpwid ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → 𝑠 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
198 uncom ⊢ ( 𝑦 ∪ { 𝑧 } ) = ( { 𝑧 } ∪ 𝑦 )
199 197 198 sseqtrdi ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → 𝑠 ⊆ ( { 𝑧 } ∪ 𝑦 ) )
200 ssundif ⊢ ( 𝑠 ⊆ ( { 𝑧 } ∪ 𝑦 ) ↔ ( 𝑠 ∖ { 𝑧 } ) ⊆ 𝑦 )
201 199 200 sylib ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → ( 𝑠 ∖ { 𝑧 } ) ⊆ 𝑦 )
202 vex ⊢ 𝑦 ∈ V
203 202 elpw2 ⊢ ( ( 𝑠 ∖ { 𝑧 } ) ∈ 𝒫 𝑦 ↔ ( 𝑠 ∖ { 𝑧 } ) ⊆ 𝑦 )
204 201 203 sylibr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → ( 𝑠 ∖ { 𝑧 } ) ∈ 𝒫 𝑦 )
205 elpwunsn ⊢ ( 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) → 𝑧 ∈ 𝑠 )
206 205 ad2antll ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → 𝑧 ∈ 𝑠 )
207 206 snssd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → { 𝑧 } ⊆ 𝑠 )
208 ssequn2 ⊢ ( { 𝑧 } ⊆ 𝑠 ↔ ( 𝑠 ∪ { 𝑧 } ) = 𝑠 )
209 207 208 sylib ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ( 𝑠 ∪ { 𝑧 } ) = 𝑠 )
210 209 eqcomd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → 𝑠 = ( 𝑠 ∪ { 𝑧 } ) )
211 uneq1 ⊢ ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) → ( 𝑢 ∪ { 𝑧 } ) = ( ( 𝑠 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
212 undif1 ⊢ ( ( 𝑠 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( 𝑠 ∪ { 𝑧 } )
213 211 212 eqtrdi ⊢ ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) → ( 𝑢 ∪ { 𝑧 } ) = ( 𝑠 ∪ { 𝑧 } ) )
214 213 eqeq2d ⊢ ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) → ( 𝑠 = ( 𝑢 ∪ { 𝑧 } ) ↔ 𝑠 = ( 𝑠 ∪ { 𝑧 } ) ) )
215 210 214 syl5ibrcom ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) → 𝑠 = ( 𝑢 ∪ { 𝑧 } ) ) )
216 176 ad2antrl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → 𝑢 ⊆ 𝑦 )
217 simpllr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
218 216 217 ssneldd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑢 )
219 difsnb ⊢ ( ¬ 𝑧 ∈ 𝑢 ↔ ( 𝑢 ∖ { 𝑧 } ) = 𝑢 )
220 218 219 sylib ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ( 𝑢 ∖ { 𝑧 } ) = 𝑢 )
221 220 eqcomd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → 𝑢 = ( 𝑢 ∖ { 𝑧 } ) )
222 difeq1 ⊢ ( 𝑠 = ( 𝑢 ∪ { 𝑧 } ) → ( 𝑠 ∖ { 𝑧 } ) = ( ( 𝑢 ∪ { 𝑧 } ) ∖ { 𝑧 } ) )
223 difun2 ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∖ { 𝑧 } ) = ( 𝑢 ∖ { 𝑧 } )
224 222 223 eqtrdi ⊢ ( 𝑠 = ( 𝑢 ∪ { 𝑧 } ) → ( 𝑠 ∖ { 𝑧 } ) = ( 𝑢 ∖ { 𝑧 } ) )
225 224 eqeq2d ⊢ ( 𝑠 = ( 𝑢 ∪ { 𝑧 } ) → ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) ↔ 𝑢 = ( 𝑢 ∖ { 𝑧 } ) ) )
226 221 225 syl5ibrcom ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ( 𝑠 = ( 𝑢 ∪ { 𝑧 } ) → 𝑢 = ( 𝑠 ∖ { 𝑧 } ) ) )
227 215 226 impbid ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ( 𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) ) → ( 𝑢 = ( 𝑠 ∖ { 𝑧 } ) ↔ 𝑠 = ( 𝑢 ∪ { 𝑧 } ) ) )
228 175 194 204 227 f1o2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑢 ∈ 𝒫 𝑦 ↦ ( 𝑢 ∪ { 𝑧 } ) ) : 𝒫 𝑦 –1-1-onto→ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) )
229 uneq1 ⊢ ( 𝑢 = 𝑡 → ( 𝑢 ∪ { 𝑧 } ) = ( 𝑡 ∪ { 𝑧 } ) )
230 vex ⊢ 𝑡 ∈ V
231 230 181 unex ⊢ ( 𝑡 ∪ { 𝑧 } ) ∈ V
232 229 175 231 fvmpt ⊢ ( 𝑡 ∈ 𝒫 𝑦 → ( ( 𝑢 ∈ 𝒫 𝑦 ↦ ( 𝑢 ∪ { 𝑧 } ) ) ‘ 𝑡 ) = ( 𝑡 ∪ { 𝑧 } ) )
233 232 adantl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑡 ∈ 𝒫 𝑦 ) → ( ( 𝑢 ∈ 𝒫 𝑦 ↦ ( 𝑢 ∪ { 𝑧 } ) ) ‘ 𝑡 ) = ( 𝑡 ∪ { 𝑧 } ) )
234 195 163 sylan2 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
235 172 174 228 233 234 fsumf1o ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = Σ 𝑡 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) )
236 uneq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∪ { 𝑧 } ) = ( 𝑠 ∪ { 𝑧 } ) )
237 236 fveq2d ⊢ ( 𝑡 = 𝑠 → ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) = ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
238 237 oveq2d ⊢ ( 𝑡 = 𝑠 → ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) )
239 inteq ⊢ ( 𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠 )
240 239 ineq1d ⊢ ( 𝑡 = 𝑠 → ( ∩ 𝑡 ∩ 𝑧 ) = ( ∩ 𝑠 ∩ 𝑧 ) )
241 240 ineq2d ⊢ ( 𝑡 = 𝑠 → ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) )
242 241 fveq2d ⊢ ( 𝑡 = 𝑠 → ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) )
243 238 242 oveq12d ⊢ ( 𝑡 = 𝑠 → ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) = ( ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
244 243 cbvsumv ⊢ Σ 𝑡 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) )
245 55 a1i ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → - 1 ∈ ℂ )
246 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦 )
247 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦 ) → 𝑠 ∈ Fin )
248 143 246 247 syl2an ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑠 ∈ Fin )
249 248 153 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
250 245 249 expp1d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) + 1 ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · - 1 ) )
251 246 adantl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑠 ⊆ 𝑦 )
252 simpllr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
253 251 252 ssneldd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ¬ 𝑧 ∈ 𝑠 )
254 hashunsng ⊢ ( 𝑧 ∈ V → ( ( 𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠 ) → ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑠 ) + 1 ) ) )
255 254 elv ⊢ ( ( 𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠 ) → ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑠 ) + 1 ) )
256 248 253 255 syl2anc ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑠 ) + 1 ) )
257 256 oveq2d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) = ( - 1 ↑ ( ( ♯ ‘ 𝑠 ) + 1 ) ) )
258 138 sseli ⊢ ( 𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
259 258 155 sylan2 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
260 245 259 mulcomd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 · ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · - 1 ) )
261 250 257 260 3eqtr4d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) = ( - 1 · ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ) )
262 259 mulm1d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 · ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ) = - ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) )
263 261 262 eqtrd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) = - ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) )
264 263 oveq1d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) = ( - ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
265 inss1 ⊢ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ⊆ 𝑥
266 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ⊆ 𝑥 ) → ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ∈ Fin )
267 156 265 266 sylancl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ∈ Fin )
268 hashcl ⊢ ( ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ∈ ℕ0 )
269 267 268 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ∈ ℕ0 )
270 269 nn0cnd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ∈ ℂ )
271 258 270 sylan2 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ∈ ℂ )
272 259 271 mulneg1d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( - ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) = - ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
273 264 272 eqtrd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) = - ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
274 273 sumeq2dv ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 - ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
275 244 274 eqtrid ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑡 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 - ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
276 155 270 mulcld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ∈ ℂ )
277 258 276 sylan2 ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ∈ ℂ )
278 174 277 fsumneg ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 𝑦 - ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) = - Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
279 235 275 278 3eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = - Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
280 279 oveq2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) + - Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
281 138 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
282 281 sselda ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
283 282 163 syldan ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
284 174 283 fsumcl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
285 282 276 syldan ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ∈ ℂ )
286 174 285 fsumcl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ∈ ℂ )
287 284 286 negsubd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) + - Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
288 164 280 287 3eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
289 288 adantr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
290 102 134 289 3eqtr4d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
291 290 ex ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
292 291 ralrimdva ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) → ∀ 𝑥 ∈ Fin ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
293 ineq1 ⊢ ( 𝑏 = 𝑥 → ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) = ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) )
294 293 fveq2d ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) )
295 67 294 oveq12d ⊢ ( 𝑏 = 𝑥 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) )
296 ineq1 ⊢ ( 𝑏 = 𝑥 → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ∩ 𝑠 ) )
297 296 fveq2d ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) )
298 297 oveq2d ⊢ ( 𝑏 = 𝑥 → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
299 298 sumeq2sdv ⊢ ( 𝑏 = 𝑥 → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
300 295 299 eqeq12d ⊢ ( 𝑏 = 𝑥 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
301 300 cbvralvw ⊢ ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑥 ∈ Fin ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
302 292 301 syl6ibr ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) → ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
303 16 24 38 46 66 302 findcard2s ⊢ ( 𝐴 ∈ Fin → ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
304 fveq2 ⊢ ( 𝑏 = 𝐵 → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ 𝐵 ) )
305 ineq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∩ ∪ 𝐴 ) = ( 𝐵 ∩ ∪ 𝐴 ) )
306 305 fveq2d ⊢ ( 𝑏 = 𝐵 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) = ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) )
307 304 306 oveq12d ⊢ ( 𝑏 = 𝐵 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) ) )
308 simpl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴 ) → 𝑏 = 𝐵 )
309 308 ineq1d ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝐵 ∩ ∩ 𝑠 ) )
310 309 fveq2d ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) )
311 310 oveq2d ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )
312 311 sumeq2dv ⊢ ( 𝑏 = 𝐵 → Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )
313 307 312 eqeq12d ⊢ ( 𝑏 = 𝐵 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) ) )
314 313 rspccva ⊢ ( ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )
315 303 314 sylan ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐵 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )