MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashbclem Structured version   Visualization version   GIF version

Theorem hashbclem 13798
Description: Lemma for hashbc 13799: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)
Hypotheses
Ref Expression
hashbc.1 (𝜑𝐴 ∈ Fin)
hashbc.2 (𝜑 → ¬ 𝑧𝐴)
hashbc.3 (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))
hashbc.4 (𝜑𝐾 ∈ ℤ)
Assertion
Ref Expression
hashbclem (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
Distinct variable groups:   𝑥,𝑗,𝑧,𝐴   𝑗,𝐾,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑧,𝑗)   𝐾(𝑧)

Proof of Theorem hashbclem
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7153 . . . . . 6 (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾))
2 eqeq2 2830 . . . . . . . 8 (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾))
32rabbidv 3478 . . . . . . 7 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})
43fveq2d 6667 . . . . . 6 (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
51, 4eqeq12d 2834 . . . . 5 (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})))
6 hashbc.3 . . . . 5 (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))
7 hashbc.4 . . . . 5 (𝜑𝐾 ∈ ℤ)
85, 6, 7rspcdva 3622 . . . 4 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
9 ssun1 4145 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
10 sspwb 5332 . . . . . . . . . . . . 13 (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
119, 10mpbi 231 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1211sseli 3960 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1312adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
14 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
15 elpwi 4547 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1615ssneld 3966 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1714, 16mpan9 507 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1813, 17jca 512 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
19 elpwi 4547 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
20 uncom 4126 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2119, 20sseqtrdi 4014 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2221adantr 481 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
23 simpr 485 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
24 disjsn 4639 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2523, 24sylibr 235 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
26 disjssun 4413 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2725, 26syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2822, 27mpbid 233 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
29 vex 3495 . . . . . . . . . . . 12 𝑥 ∈ V
3029elpw 4542 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3128, 30sylibr 235 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3231adantl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3318, 32impbida 797 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3433anbi1d 629 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾)))
35 anass 469 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
3634, 35syl6bb 288 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))))
3736rabbidva2 3474 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
3837fveq2d 6667 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
398, 38eqtrd 2853 . . 3 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
40 oveq2 7153 . . . . . 6 (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1)))
41 eqeq2 2830 . . . . . . . 8 (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1)))
4241rabbidv 3478 . . . . . . 7 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
4342fveq2d 6667 . . . . . 6 (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
4440, 43eqeq12d 2834 . . . . 5 (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})))
45 peano2zm 12013 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
467, 45syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
4744, 6, 46rspcdva 3622 . . . 4 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
48 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
49 pwfi 8807 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
5048, 49sylib 219 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
51 rabexg 5225 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
5250, 51syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
53 snfi 8582 . . . . . . . . . 10 {𝑧} ∈ Fin
54 unfi 8773 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5548, 53, 54sylancl 586 . . . . . . . . 9 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
56 pwfi 8807 . . . . . . . . 9 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5755, 56sylib 219 . . . . . . . 8 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
58 ssrab2 4053 . . . . . . . 8 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
59 ssfi 8726 . . . . . . . 8 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
6057, 58, 59sylancl 586 . . . . . . 7 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
6160elexd 3512 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V)
62 fveqeq2 6672 . . . . . . . 8 (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1)))
6362elrab 3677 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)))
64 eleq2 2898 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
65 fveqeq2 6672 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
6664, 65anbi12d 630 . . . . . . . . 9 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)))
67 elpwi 4547 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6867ad2antrl 724 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
69 unss1 4152 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7068, 69syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
71 vex 3495 . . . . . . . . . . . 12 𝑢 ∈ V
72 snex 5322 . . . . . . . . . . . 12 {𝑧} ∈ V
7371, 72unex 7458 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7473elpw 4542 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7570, 74sylibr 235 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7648adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
7776, 68ssfid 8729 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
7853a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
7914adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
8068, 79ssneldd 3967 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
81 disjsn 4639 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8280, 81sylibr 235 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
83 hashun 13731 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
8477, 78, 82, 83syl3anc 1363 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
85 simprr 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1))
86 hashsng 13718 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (♯‘{𝑧}) = 1)
8786elv 3497 . . . . . . . . . . . . 13 (♯‘{𝑧}) = 1
8887a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1)
8985, 88oveq12d 7163 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1))
907adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
9190zcnd 12076 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
92 ax-1cn 10583 . . . . . . . . . . . 12 1 ∈ ℂ
93 npcan 10883 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9491, 92, 93sylancl 586 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9584, 89, 943eqtrd 2857 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾)
96 ssun2 4146 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
97 vex 3495 . . . . . . . . . . . 12 𝑧 ∈ V
9897snss 4710 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
9996, 98mpbir 232 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
10095, 99jctil 520 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
10166, 75, 100elrabd 3679 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
102101ex 413 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
10363, 102syl5bi 243 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
104 eleq2 2898 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
105 fveqeq2 6672 . . . . . . . . 9 (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾))
106104, 105anbi12d 630 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
107106elrab 3677 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
108 fveqeq2 6672 . . . . . . . . 9 (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
109 elpwi 4547 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
110109ad2antrl 724 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
111110, 20sseqtrdi 4014 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
112 ssundif 4429 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
113111, 112sylib 219 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
114 vex 3495 . . . . . . . . . . . 12 𝑣 ∈ V
115114difexi 5223 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
116115elpw 4542 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
117113, 116sylibr 235 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
11848adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
119118, 113ssfid 8729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
120 hashcl 13705 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
121119, 120syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
122121nn0cnd 11945 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ)
123 pncan 10880 . . . . . . . . . . 11 (((♯‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
124122, 92, 123sylancl 586 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
125 undif1 4420 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
126 simprrl 777 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
127126snssd 4734 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
128 ssequn2 4156 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
129127, 128sylib 219 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
130125, 129syl5eq 2865 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
131130fveq2d 6667 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣))
13253a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
133 incom 4175 . . . . . . . . . . . . . . . 16 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
134 disjdif 4417 . . . . . . . . . . . . . . . 16 ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
135133, 134eqtri 2841 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
136135a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
137 hashun 13731 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
138119, 132, 136, 137syl3anc 1363 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
13987oveq2i 7156 . . . . . . . . . . . . 13 ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)
140138, 139syl6eq 2869 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1))
141 simprrr 778 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾)
142131, 140, 1413eqtr3d 2861 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
143142oveq1d 7160 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
144124, 143eqtr3d 2855 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
145108, 117, 144elrabd 3679 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
146145ex 413 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
147107, 146syl5bi 243 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
14863, 107anbi12i 626 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))))
149 simp3rl 1238 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
150149snssd 4734 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
151 incom 4175 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
152823adant3 1124 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
153151, 152syl5eq 2865 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
154 uneqdifeq 4434 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
155150, 153, 154syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
156155bicomd 224 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
157 eqcom 2825 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
158 eqcom 2825 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
159 uncom 4126 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
160159eqeq1i 2823 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
161158, 160bitri 276 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
162156, 157, 1613bitr4g 315 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1631623expib 1114 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
164148, 163syl5bi 243 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
16552, 61, 103, 147, 164en3d 8534 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
166 ssrab2 4053 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
167 ssfi 8726 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
16850, 166, 167sylancl 586 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
169 hashen 13695 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
170168, 60, 169syl2anc 584 . . . . 5 (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
171165, 170mpbird 258 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
17247, 171eqtrd 2853 . . 3 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
17339, 172oveq12d 7163 . 2 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
17453a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
175 disjsn 4639 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
17614, 175sylibr 235 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
177 hashun 13731 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17848, 174, 176, 177syl3anc 1363 . . . . 5 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17987oveq2i 7156 . . . . 5 ((♯‘𝐴) + (♯‘{𝑧})) = ((♯‘𝐴) + 1)
180178, 179syl6eq 2869 . . . 4 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1))
181180oveq1d 7160 . . 3 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾))
182 hashcl 13705 . . . . 5 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
18348, 182syl 17 . . . 4 (𝜑 → (♯‘𝐴) ∈ ℕ0)
184 bcpasc 13669 . . . 4 (((♯‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
185183, 7, 184syl2anc 584 . . 3 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
186181, 185eqtr4d 2856 . 2 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))))
187 pm2.1 890 . . . . . . . 8 𝑧𝑥𝑧𝑥)
188187biantrur 531 . . . . . . 7 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾))
189 andir 1002 . . . . . . 7 (((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
190188, 189bitri 276 . . . . . 6 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
191190rabbii 3471 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
192 unrab 4271 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
193191, 192eqtr4i 2844 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
194193fveq2i 6666 . . 3 (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
195 ssrab2 4053 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
196 ssfi 8726 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
19757, 195, 196sylancl 586 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
198 inrab 4272 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
199 simprl 767 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧𝑥)
200 simpll 763 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
201199, 200pm2.65i 195 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
202201rgenw 3147 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
203 rabeq0 4335 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
204202, 203mpbir 232 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅
205198, 204eqtri 2841 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅
206205a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅)
207 hashun 13731 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
208197, 60, 206, 207syl3anc 1363 . . 3 (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
209194, 208syl5eq 2865 . 2 (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
210173, 186, 2093eqtr4d 2863 1 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wral 3135  {crab 3139  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   class class class wbr 5057  cfv 6348  (class class class)co 7145  cen 8494  Fincfn 8497  cc 10523  1c1 10526   + caddc 10528  cmin 10858  0cn0 11885  cz 11969  Ccbc 13650  chash 13678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12881  df-seq 13358  df-fac 13622  df-bc 13651  df-hash 13679
This theorem is referenced by:  hashbc  13799
  Copyright terms: Public domain W3C validator