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 unisnv ⊢ ∪ { 𝑧 } = 𝑧
28 27 uneq2i ⊢ ( ∪ 𝑦 ∪ ∪ { 𝑧 } ) = ( ∪ 𝑦 ∪ 𝑧 )
29 26 28 eqtri ⊢ ∪ ( 𝑦 ∪ { 𝑧 } ) = ( ∪ 𝑦 ∪ 𝑧 )
30 25 29 eqtrdi ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑥 = ( ∪ 𝑦 ∪ 𝑧 ) )
31 30 ineq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) )
32 31 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) )
33 32 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) )
34 pweq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → 𝒫 𝑥 = 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
35 34 sumeq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
36 33 35 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
37 36 ralbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
38 unieq ⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
39 38 ineq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑏 ∩ ∪ 𝑥 ) = ( 𝑏 ∩ ∪ 𝐴 ) )
40 39 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) = ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) )
41 40 oveq2d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) )
42 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
43 42 sumeq1d ⊢ ( 𝑥 = 𝐴 → Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
44 41 43 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
45 44 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑥 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑥 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝐴 ) ) ) = Σ 𝑠 ∈ 𝒫 𝐴 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
46 hashcl ⊢ ( 𝑏 ∈ Fin → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
47 46 nn0cnd ⊢ ( 𝑏 ∈ Fin → ( ♯ ‘ 𝑏 ) ∈ ℂ )
48 47 mullidd ⊢ ( 𝑏 ∈ Fin → ( 1 · ( ♯ ‘ 𝑏 ) ) = ( ♯ ‘ 𝑏 ) )
49 0ex ⊢ ∅ ∈ V
50 48 47 eqeltrd ⊢ ( 𝑏 ∈ Fin → ( 1 · ( ♯ ‘ 𝑏 ) ) ∈ ℂ )
51 fveq2 ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ∅ ) )
52 51 8 eqtrdi ⊢ ( 𝑠 = ∅ → ( ♯ ‘ 𝑠 ) = 0 )
53 52 oveq2d ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( - 1 ↑ 0 ) )
54 neg1cn ⊢ - 1 ∈ ℂ
55 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
56 54 55 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
57 53 56 eqtrdi ⊢ ( 𝑠 = ∅ → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = 1 )
58 rint0 ⊢ ( 𝑠 = ∅ → ( 𝑏 ∩ ∩ 𝑠 ) = 𝑏 )
59 58 fveq2d ⊢ ( 𝑠 = ∅ → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ 𝑏 ) )
60 57 59 oveq12d ⊢ ( 𝑠 = ∅ → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
61 60 sumsn ⊢ ( ( ∅ ∈ V ∧ ( 1 · ( ♯ ‘ 𝑏 ) ) ∈ ℂ ) → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
62 49 50 61 sylancr ⊢ ( 𝑏 ∈ Fin → Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( 1 · ( ♯ ‘ 𝑏 ) ) )
63 47 subid1d ⊢ ( 𝑏 ∈ Fin → ( ( ♯ ‘ 𝑏 ) − 0 ) = ( ♯ ‘ 𝑏 ) )
64 48 62 63 3eqtr4rd ⊢ ( 𝑏 ∈ Fin → ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) )
65 64 rgen ⊢ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − 0 ) = Σ 𝑠 ∈ { ∅ } ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) )
66 fveq2 ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ 𝑥 ) )
67 ineq1 ⊢ ( 𝑏 = 𝑥 → ( 𝑏 ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ∪ 𝑦 ) )
68 67 fveq2d ⊢ ( 𝑏 = 𝑥 → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) = ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) )
69 66 68 oveq12d ⊢ ( 𝑏 = 𝑥 → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) )
70 simpl ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑏 = 𝑥 )
71 70 ineq1d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ∩ 𝑠 ) )
72 71 fveq2d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) )
73 72 oveq2d ⊢ ( ( 𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
74 73 sumeq2dv ⊢ ( 𝑏 = 𝑥 → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
75 69 74 eqeq12d ⊢ ( 𝑏 = 𝑥 → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
76 75 rspcva ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
77 76 adantll ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) )
78 simpr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝑥 ∈ Fin )
79 inss1 ⊢ ( 𝑥 ∩ 𝑧 ) ⊆ 𝑥
80 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝑧 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑧 ) ∈ Fin )
81 78 79 80 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ 𝑧 ) ∈ Fin )
82 fveq2 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) )
83 ineq1 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∪ 𝑦 ) = ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) )
84 in32 ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ 𝑧 )
85 inass ⊢ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ 𝑧 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) )
86 84 85 eqtri ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) )
87 83 86 eqtrdi ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∪ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) )
88 87 fveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) )
89 82 88 oveq12d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) )
90 ineq1 ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) )
91 in32 ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) = ( ( 𝑥 ∩ ∩ 𝑠 ) ∩ 𝑧 )
92 inass ⊢ ( ( 𝑥 ∩ ∩ 𝑠 ) ∩ 𝑧 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) )
93 91 92 eqtri ⊢ ( ( 𝑥 ∩ 𝑧 ) ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) )
94 90 93 eqtrdi ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( 𝑏 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) )
95 94 fveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) )
96 95 oveq2d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
97 96 sumeq2sdv ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
98 89 97 eqeq12d ⊢ ( 𝑏 = ( 𝑥 ∩ 𝑧 ) → ( ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ↔ ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
99 98 rspcva ⊢ ( ( ( 𝑥 ∩ 𝑧 ) ∈ Fin ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
100 81 99 sylan ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) )
101 77 100 oveq12d ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
102 inss1 ⊢ ( 𝑥 ∩ ∪ 𝑦 ) ⊆ 𝑥
103 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ∪ 𝑦 ) ⊆ 𝑥 ) → ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin )
104 78 102 103 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin )
105 hashcl ⊢ ( ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℕ0 )
106 104 105 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℕ0 )
107 106 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ∈ ℂ )
108 hashcl ⊢ ( ( 𝑥 ∩ 𝑧 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℕ0 )
109 81 108 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℕ0 )
110 109 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ∈ ℂ )
111 inss1 ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ⊆ 𝑥
112 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ⊆ 𝑥 ) → ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin )
113 78 111 112 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin )
114 hashcl ⊢ ( ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℕ0 )
115 113 114 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℕ0 )
116 115 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ∈ ℂ )
117 hashun3 ⊢ ( ( ( 𝑥 ∩ ∪ 𝑦 ) ∈ Fin ∧ ( 𝑥 ∩ 𝑧 ) ∈ Fin ) → ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) ) )
118 104 81 117 syl2anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) ) )
119 indi ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) )
120 119 fveq2i ⊢ ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∪ ( 𝑥 ∩ 𝑧 ) ) )
121 inindi ⊢ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) = ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) )
122 121 fveq2i ⊢ ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) = ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) )
123 122 oveq2i ⊢ ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( ( 𝑥 ∩ ∪ 𝑦 ) ∩ ( 𝑥 ∩ 𝑧 ) ) ) )
124 118 120 123 3eqtr4g ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) )
125 107 110 116 124 assraddsubd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) = ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
126 125 oveq2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) ) )
127 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
128 127 adantl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
129 128 nn0cnd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ 𝑥 ) ∈ ℂ )
130 110 116 subcld ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ∈ ℂ )
131 129 107 130 subsub4d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) = ( ( ♯ ‘ 𝑥 ) − ( ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) + ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) ) )
132 126 131 eqtr4d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
133 132 adantr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = ( ( ( ♯ ‘ 𝑥 ) − ( ♯ ‘ ( 𝑥 ∩ ∪ 𝑦 ) ) ) − ( ( ♯ ‘ ( 𝑥 ∩ 𝑧 ) ) − ( ♯ ‘ ( 𝑥 ∩ ( ∪ 𝑦 ∩ 𝑧 ) ) ) ) ) )
134 disjdif ⊢ ( 𝒫 𝑦 ∩ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = ∅
135 134 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝒫 𝑦 ∩ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = ∅ )
136 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
137 136 sspwi ⊢ 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } )
138 undif ⊢ ( 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
139 137 138 mpbi ⊢ ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) = 𝒫 ( 𝑦 ∪ { 𝑧 } )
140 139 eqcomi ⊢ 𝒫 ( 𝑦 ∪ { 𝑧 } ) = ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) )
141 140 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 ( 𝑦 ∪ { 𝑧 } ) = ( 𝒫 𝑦 ∪ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ) )
142 simpll ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝑦 ∈ Fin )
143 snfi ⊢ { 𝑧 } ∈ Fin
144 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
145 142 143 144 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
146 pwfi ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ↔ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
147 145 146 sylib ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
148 54 a1i ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → - 1 ∈ ℂ )
149 elpwi ⊢ ( 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) → 𝑠 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
150 ssfi ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 𝑠 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑠 ∈ Fin )
151 145 149 150 syl2an ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → 𝑠 ∈ Fin )
152 hashcl ⊢ ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
153 151 152 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
154 148 153 expcld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) ∈ ℂ )
155 simplr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → 𝑥 ∈ Fin )
156 inss1 ⊢ ( 𝑥 ∩ ∩ 𝑠 ) ⊆ 𝑥
157 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ ∩ 𝑠 ) ⊆ 𝑥 ) → ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin )
158 155 156 157 sylancl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin )
159 hashcl ⊢ ( ( 𝑥 ∩ ∩ 𝑠 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
160 158 159 syl ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℕ0 )
161 160 nn0cnd ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ∈ ℂ )
162 154 161 mulcld ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ∈ ℂ )
163 135 141 147 162 fsumsplit ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) + Σ 𝑠 ∈ ( 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∖ 𝒫 𝑦 ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) ) )
164 fveq2 ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) )
165 164 oveq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) = ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) )
166 inteq ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ∩ 𝑠 = ∩ ( 𝑡 ∪ { 𝑧 } ) )
167 vex ⊢ 𝑧 ∈ V
168 167 intunsn ⊢ ∩ ( 𝑡 ∪ { 𝑧 } ) = ( ∩ 𝑡 ∩ 𝑧 )
169 166 168 eqtrdi ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ∩ 𝑠 = ( ∩ 𝑡 ∩ 𝑧 ) )
170 169 ineq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( 𝑥 ∩ ∩ 𝑠 ) = ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) )
171 170 fveq2d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) = ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) )
172 165 171 oveq12d ⊢ ( 𝑠 = ( 𝑡 ∪ { 𝑧 } ) → ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( ( - 1 ↑ ( ♯ ‘ ( 𝑡 ∪ { 𝑧 } ) ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑡 ∩ 𝑧 ) ) ) ) )
173 pwfi ⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin )
174 142 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 vsnex ⊢ { 𝑧 } ∈ V
182 180 181 unex ⊢ ( 𝑢 ∪ { 𝑧 } ) ∈ V
183 182 elpw ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
184 179 183 sylibr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
185 simpllr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑢 ∈ 𝒫 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
186 elpwi ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 𝑦 → ( 𝑢 ∪ { 𝑧 } ) ⊆ 𝑦 )
187 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑢 ∪ { 𝑧 } )
188 167 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 162 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 54 a1i ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → - 1 ∈ ℂ )
246 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦 )
247 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦 ) → 𝑠 ∈ Fin )
248 142 246 247 syl2an ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑠 ∈ Fin )
249 248 152 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 137 sseli ⊢ ( 𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
259 258 154 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 155 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 154 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 137 a1i ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → 𝒫 𝑦 ⊆ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
282 281 sselda ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
283 282 162 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 163 280 287 3eqtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
289 288 adantr ⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑥 ∈ Fin ) ∧ ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) → Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) = ( Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ∩ 𝑠 ) ) ) − Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑥 ∩ ( ∩ 𝑠 ∩ 𝑧 ) ) ) ) ) )
290 101 133 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 66 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 imbitrrdi ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ∪ 𝑦 ) ) ) = Σ 𝑠 ∈ 𝒫 𝑦 ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) → ∀ 𝑏 ∈ Fin ( ( ♯ ‘ 𝑏 ) − ( ♯ ‘ ( 𝑏 ∩ ( ∪ 𝑦 ∪ 𝑧 ) ) ) ) = Σ 𝑠 ∈ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ( ( - 1 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝑏 ∩ ∩ 𝑠 ) ) ) ) )
303 16 24 37 45 65 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 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 ∩ ∩ 𝑠 ) ) ) )