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 syl6ibr ( ( 𝑦 ∈ 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 ↑ ( ♯ ‘ 𝑠 ) ) · ( ♯ ‘ ( 𝐵 𝑠 ) ) ) )