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

Theorem hashbclem 13554
 Description: Lemma for hashbc 13555: 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 6932 . . . . . 6 (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾))
2 eqeq2 2789 . . . . . . . 8 (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾))
32rabbidv 3386 . . . . . . 7 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})
43fveq2d 6452 . . . . . 6 (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
51, 4eqeq12d 2793 . . . . 5 (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})))
6 hashbc.3 . . . . 5 (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))
7 hashbc.4 . . . . 5 (𝜑𝐾 ∈ ℤ)
85, 6, 7rspcdva 3517 . . . 4 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
9 ssun1 3999 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
10 sspwb 5151 . . . . . . . . . . . . 13 (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
119, 10mpbi 222 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1211sseli 3817 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1312adantl 475 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
14 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
15 elpwi 4389 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1615ssneld 3823 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1714, 16mpan9 502 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1813, 17jca 507 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
19 elpwi 4389 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
20 uncom 3980 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2119, 20syl6sseq 3870 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2221adantr 474 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
23 simpr 479 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
24 disjsn 4478 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2523, 24sylibr 226 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
26 disjssun 4260 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2725, 26syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2822, 27mpbid 224 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
29 vex 3401 . . . . . . . . . . . 12 𝑥 ∈ V
3029elpw 4385 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3128, 30sylibr 226 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3231adantl 475 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3318, 32impbida 791 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3433anbi1d 623 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾)))
35 anass 462 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
3634, 35syl6bb 279 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))))
3736rabbidva2 3383 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
3837fveq2d 6452 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
398, 38eqtrd 2814 . . 3 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
40 oveq2 6932 . . . . . 6 (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1)))
41 eqeq2 2789 . . . . . . . 8 (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1)))
4241rabbidv 3386 . . . . . . 7 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
4342fveq2d 6452 . . . . . 6 (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
4440, 43eqeq12d 2793 . . . . 5 (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})))
45 peano2zm 11776 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
467, 45syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
4744, 6, 46rspcdva 3517 . . . 4 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
48 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
49 pwfi 8551 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
5048, 49sylib 210 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
51 rabexg 5050 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
5250, 51syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
53 snfi 8328 . . . . . . . . . 10 {𝑧} ∈ Fin
54 unfi 8517 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5548, 53, 54sylancl 580 . . . . . . . . 9 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
56 pwfi 8551 . . . . . . . . 9 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5755, 56sylib 210 . . . . . . . 8 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
58 ssrab2 3908 . . . . . . . 8 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
59 ssfi 8470 . . . . . . . 8 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
6057, 58, 59sylancl 580 . . . . . . 7 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
6160elexd 3416 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V)
62 fveqeq2 6457 . . . . . . . 8 (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1)))
6362elrab 3572 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)))
64 eleq2 2848 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
65 fveqeq2 6457 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
6664, 65anbi12d 624 . . . . . . . . 9 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)))
67 elpwi 4389 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6867ad2antrl 718 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
69 unss1 4005 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7068, 69syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
71 vex 3401 . . . . . . . . . . . 12 𝑢 ∈ V
72 snex 5142 . . . . . . . . . . . 12 {𝑧} ∈ V
7371, 72unex 7235 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7473elpw 4385 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7570, 74sylibr 226 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7648adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
7776, 68ssfid 8473 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
7853a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
7914adantr 474 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
8068, 79ssneldd 3824 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
81 disjsn 4478 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8280, 81sylibr 226 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
83 hashun 13490 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
8477, 78, 82, 83syl3anc 1439 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
85 simprr 763 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1))
86 hashsng 13478 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (♯‘{𝑧}) = 1)
8786elv 3402 . . . . . . . . . . . . 13 (♯‘{𝑧}) = 1
8887a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1)
8985, 88oveq12d 6942 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1))
907adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
9190zcnd 11839 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
92 ax-1cn 10332 . . . . . . . . . . . 12 1 ∈ ℂ
93 npcan 10634 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9491, 92, 93sylancl 580 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9584, 89, 943eqtrd 2818 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾)
96 ssun2 4000 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
97 vex 3401 . . . . . . . . . . . 12 𝑧 ∈ V
9897snss 4549 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
9996, 98mpbir 223 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
10095, 99jctil 515 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
10166, 75, 100elrabd 3575 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
102101ex 403 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
10363, 102syl5bi 234 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
104 eleq2 2848 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
105 fveqeq2 6457 . . . . . . . . 9 (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾))
106104, 105anbi12d 624 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
107106elrab 3572 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
108 fveqeq2 6457 . . . . . . . . 9 (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
109 elpwi 4389 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
110109ad2antrl 718 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
111110, 20syl6sseq 3870 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
112 ssundif 4276 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
113111, 112sylib 210 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
114 vex 3401 . . . . . . . . . . . 12 𝑣 ∈ V
115114difexi 5048 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
116115elpw 4385 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
117113, 116sylibr 226 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
11848adantr 474 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
119118, 113ssfid 8473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
120 hashcl 13466 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
121119, 120syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
122121nn0cnd 11708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ)
123 pncan 10630 . . . . . . . . . . 11 (((♯‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
124122, 92, 123sylancl 580 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
125 undif1 4267 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
126 simprrl 771 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
127126snssd 4573 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
128 ssequn2 4009 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
129127, 128sylib 210 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
130125, 129syl5eq 2826 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
131130fveq2d 6452 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣))
13253a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
133 incom 4028 . . . . . . . . . . . . . . . 16 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
134 disjdif 4264 . . . . . . . . . . . . . . . 16 ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
135133, 134eqtri 2802 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
136135a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
137 hashun 13490 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
138119, 132, 136, 137syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
13987oveq2i 6935 . . . . . . . . . . . . 13 ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)
140138, 139syl6eq 2830 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1))
141 simprrr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾)
142131, 140, 1413eqtr3d 2822 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
143142oveq1d 6939 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
144124, 143eqtr3d 2816 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
145108, 117, 144elrabd 3575 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
146145ex 403 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
147107, 146syl5bi 234 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
14863, 107anbi12i 620 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))))
149 simp3rl 1284 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
150149snssd 4573 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
151 incom 4028 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
152823adant3 1123 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
153151, 152syl5eq 2826 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
154 uneqdifeq 4281 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
155150, 153, 154syl2anc 579 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
156155bicomd 215 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
157 eqcom 2785 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
158 eqcom 2785 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
159 uncom 3980 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
160159eqeq1i 2783 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
161158, 160bitri 267 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
162156, 157, 1613bitr4g 306 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1631623expib 1113 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
164148, 163syl5bi 234 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
16552, 61, 103, 147, 164en3d 8280 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
166 ssrab2 3908 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
167 ssfi 8470 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
16850, 166, 167sylancl 580 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
169 hashen 13456 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
170168, 60, 169syl2anc 579 . . . . 5 (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
171165, 170mpbird 249 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
17247, 171eqtrd 2814 . . 3 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
17339, 172oveq12d 6942 . 2 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
17453a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
175 disjsn 4478 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
17614, 175sylibr 226 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
177 hashun 13490 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17848, 174, 176, 177syl3anc 1439 . . . . 5 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17987oveq2i 6935 . . . . 5 ((♯‘𝐴) + (♯‘{𝑧})) = ((♯‘𝐴) + 1)
180178, 179syl6eq 2830 . . . 4 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1))
181180oveq1d 6939 . . 3 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾))
182 hashcl 13466 . . . . 5 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
18348, 182syl 17 . . . 4 (𝜑 → (♯‘𝐴) ∈ ℕ0)
184 bcpasc 13430 . . . 4 (((♯‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
185183, 7, 184syl2anc 579 . . 3 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
186181, 185eqtr4d 2817 . 2 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))))
187 pm2.1 883 . . . . . . . 8 𝑧𝑥𝑧𝑥)
188187biantrur 526 . . . . . . 7 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾))
189 andir 994 . . . . . . 7 (((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
190188, 189bitri 267 . . . . . 6 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
191190rabbii 3382 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
192 unrab 4124 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
193191, 192eqtr4i 2805 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
194193fveq2i 6451 . . 3 (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
195 ssrab2 3908 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
196 ssfi 8470 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
19757, 195, 196sylancl 580 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
198 inrab 4125 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
199 simprl 761 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧𝑥)
200 simpll 757 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
201199, 200pm2.65i 186 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
202201rgenw 3106 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
203 rabeq0 4187 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
204202, 203mpbir 223 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅
205198, 204eqtri 2802 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅
206205a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅)
207 hashun 13490 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
208197, 60, 206, 207syl3anc 1439 . . 3 (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
209194, 208syl5eq 2826 . 2 (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
210173, 186, 2093eqtr4d 2824 1 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  ∀wral 3090  {crab 3094  Vcvv 3398   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  𝒫 cpw 4379  {csn 4398   class class class wbr 4888  ‘cfv 6137  (class class class)co 6924   ≈ cen 8240  Fincfn 8243  ℂcc 10272  1c1 10275   + caddc 10277   − cmin 10608  ℕ0cn0 11646  ℤcz 11732  Ccbc 13411  ♯chash 13439 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-n0 11647  df-z 11733  df-uz 11997  df-rp 12142  df-fz 12648  df-seq 13124  df-fac 13383  df-bc 13412  df-hash 13440 This theorem is referenced by:  hashbc  13555
 Copyright terms: Public domain W3C validator