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

Theorem hashbclem 13274
Description: Lemma for hashbc 13275: 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 hashbc.4 . . . . 5 (𝜑𝐾 ∈ ℤ)
2 hashbc.3 . . . . 5 (𝜑 → ∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}))
3 oveq2 6698 . . . . . . 7 (𝑗 = 𝐾 → ((#‘𝐴)C𝑗) = ((#‘𝐴)C𝐾))
4 eqeq2 2662 . . . . . . . . 9 (𝑗 = 𝐾 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = 𝐾))
54rabbidv 3220 . . . . . . . 8 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})
65fveq2d 6233 . . . . . . 7 (𝑗 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
73, 6eqeq12d 2666 . . . . . 6 (𝑗 = 𝐾 → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
87rspcv 3336 . . . . 5 (𝐾 ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
91, 2, 8sylc 65 . . . 4 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
10 ssun1 3809 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
11 sspwb 4947 . . . . . . . . . . . . 13 (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
1210, 11mpbi 220 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1312sseli 3632 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1413adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
15 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
16 elpwi 4201 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1716ssneld 3638 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1815, 17mpan9 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1914, 18jca 553 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
20 elpwi 4201 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
21 uncom 3790 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2220, 21syl6sseq 3684 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2322adantr 480 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
24 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
25 disjsn 4278 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2624, 25sylibr 224 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
27 disjssun 4069 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2826, 27syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2923, 28mpbid 222 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
30 vex 3234 . . . . . . . . . . . 12 𝑥 ∈ V
3130elpw 4197 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3229, 31sylibr 224 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3332adantl 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3419, 33impbida 895 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3534anbi1d 741 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾)))
36 anass 682 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
3735, 36syl6bb 276 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾))))
3837rabbidva2 3217 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
3938fveq2d 6233 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
409, 39eqtrd 2685 . . 3 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
41 peano2zm 11458 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
421, 41syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
43 oveq2 6698 . . . . . . 7 (𝑗 = (𝐾 − 1) → ((#‘𝐴)C𝑗) = ((#‘𝐴)C(𝐾 − 1)))
44 eqeq2 2662 . . . . . . . . 9 (𝑗 = (𝐾 − 1) → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = (𝐾 − 1)))
4544rabbidv 3220 . . . . . . . 8 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
4645fveq2d 6233 . . . . . . 7 (𝑗 = (𝐾 − 1) → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
4743, 46eqeq12d 2666 . . . . . 6 (𝑗 = (𝐾 − 1) → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4847rspcv 3336 . . . . 5 ((𝐾 − 1) ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4942, 2, 48sylc 65 . . . 4 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
50 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
51 pwfi 8302 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
5250, 51sylib 208 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
53 rabexg 4844 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
5452, 53syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
55 snfi 8079 . . . . . . . . . 10 {𝑧} ∈ Fin
56 unfi 8268 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5750, 55, 56sylancl 695 . . . . . . . . 9 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
58 pwfi 8302 . . . . . . . . 9 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5957, 58sylib 208 . . . . . . . 8 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
60 ssrab2 3720 . . . . . . . 8 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
61 ssfi 8221 . . . . . . . 8 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
6259, 60, 61sylancl 695 . . . . . . 7 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
63 elex 3243 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
6462, 63syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
65 fveq2 6229 . . . . . . . . 9 (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
6665eqeq1d 2653 . . . . . . . 8 (𝑥 = 𝑢 → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘𝑢) = (𝐾 − 1)))
6766elrab 3396 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)))
68 elpwi 4201 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6968ad2antrl 764 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
70 unss1 3815 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7169, 70syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
72 vex 3234 . . . . . . . . . . . 12 𝑢 ∈ V
73 snex 4938 . . . . . . . . . . . 12 {𝑧} ∈ V
7472, 73unex 6998 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7574elpw 4197 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7671, 75sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7750adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
78 ssfi 8221 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑢𝐴) → 𝑢 ∈ Fin)
7977, 69, 78syl2anc 694 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
8055a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
8115adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
8269, 81ssneldd 3639 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
83 disjsn 4278 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8482, 83sylibr 224 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
85 hashun 13209 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
8679, 80, 84, 85syl3anc 1366 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
87 simprr 811 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘𝑢) = (𝐾 − 1))
88 vex 3234 . . . . . . . . . . . . . 14 𝑧 ∈ V
89 hashsng 13197 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (#‘{𝑧}) = 1)
9088, 89ax-mp 5 . . . . . . . . . . . . 13 (#‘{𝑧}) = 1
9190a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘{𝑧}) = 1)
9287, 91oveq12d 6708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((#‘𝑢) + (#‘{𝑧})) = ((𝐾 − 1) + 1))
931adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
9493zcnd 11521 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
95 ax-1cn 10032 . . . . . . . . . . . 12 1 ∈ ℂ
96 npcan 10328 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9794, 95, 96sylancl 695 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9886, 92, 973eqtrd 2689 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = 𝐾)
99 ssun2 3810 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
10088snss 4348 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
10199, 100mpbir 221 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
10298, 101jctil 559 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
103 eleq2 2719 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
104 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = (𝑢 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑧})))
105104eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
106103, 105anbi12d 747 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
107106elrab 3396 . . . . . . . . 9 ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
10876, 102, 107sylanbrc 699 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
109108ex 449 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
11067, 109syl5bi 232 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
111 eleq2 2719 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
112 fveq2 6229 . . . . . . . . . 10 (𝑥 = 𝑣 → (#‘𝑥) = (#‘𝑣))
113112eqeq1d 2653 . . . . . . . . 9 (𝑥 = 𝑣 → ((#‘𝑥) = 𝐾 ↔ (#‘𝑣) = 𝐾))
114111, 113anbi12d 747 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
115114elrab 3396 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
116 elpwi 4201 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
117116ad2antrl 764 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
118117, 21syl6sseq 3684 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
119 ssundif 4085 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
120118, 119sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
121 vex 3234 . . . . . . . . . . . 12 𝑣 ∈ V
122 difexg 4841 . . . . . . . . . . . 12 (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V)
123121, 122ax-mp 5 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
124123elpw 4197 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
125120, 124sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
12650adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
127 ssfi 8221 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin)
128126, 120, 127syl2anc 694 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
129 hashcl 13185 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
130128, 129syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
131130nn0cnd 11391 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℂ)
132 pncan 10325 . . . . . . . . . . 11 (((#‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
133131, 95, 132sylancl 695 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
134 undif1 4076 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
135 simprrl 821 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
136135snssd 4372 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
137 ssequn2 3819 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
138136, 137sylib 208 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
139134, 138syl5eq 2697 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
140139fveq2d 6233 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (#‘𝑣))
14155a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
142 incom 3838 . . . . . . . . . . . . . . . 16 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
143 disjdif 4073 . . . . . . . . . . . . . . . 16 ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
144142, 143eqtri 2673 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
145144a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
146 hashun 13209 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
147128, 141, 145, 146syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
14890oveq2i 6701 . . . . . . . . . . . . 13 ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1)
149147, 148syl6eq 2701 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1))
150 simprrr 822 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘𝑣) = 𝐾)
151140, 149, 1503eqtr3d 2693 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((#‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
152151oveq1d 6705 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
153133, 152eqtr3d 2687 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
154 fveq2 6229 . . . . . . . . . . 11 (𝑥 = (𝑣 ∖ {𝑧}) → (#‘𝑥) = (#‘(𝑣 ∖ {𝑧})))
155154eqeq1d 2653 . . . . . . . . . 10 (𝑥 = (𝑣 ∖ {𝑧}) → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
156155elrab 3396 . . . . . . . . 9 ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
157125, 153, 156sylanbrc 699 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
158157ex 449 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
159115, 158syl5bi 232 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
16067, 115anbi12i 733 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))))
161 simp3rl 1154 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
162161snssd 4372 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
163 incom 3838 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
164843adant3 1101 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
165163, 164syl5eq 2697 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
166 uneqdifeq 4090 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
167162, 165, 166syl2anc 694 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
168167bicomd 213 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
169 eqcom 2658 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
170 eqcom 2658 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
171 uncom 3790 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
172171eqeq1i 2656 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
173170, 172bitri 264 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
174168, 169, 1733bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1751743expib 1287 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
176160, 175syl5bi 232 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
17754, 64, 110, 159, 176en3d 8034 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
178 ssrab2 3720 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
179 ssfi 8221 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
18052, 178, 179sylancl 695 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
181 hashen 13175 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin) → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
182180, 62, 181syl2anc 694 . . . . 5 (𝜑 → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
183177, 182mpbird 247 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18449, 183eqtrd 2685 . . 3 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18540, 184oveq12d 6708 . 2 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
18655a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
187 disjsn 4278 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
18815, 187sylibr 224 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
189 hashun 13209 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19050, 186, 188, 189syl3anc 1366 . . . . 5 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19190oveq2i 6701 . . . . 5 ((#‘𝐴) + (#‘{𝑧})) = ((#‘𝐴) + 1)
192190, 191syl6eq 2701 . . . 4 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + 1))
193192oveq1d 6705 . . 3 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴) + 1)C𝐾))
194 hashcl 13185 . . . . 5 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
19550, 194syl 17 . . . 4 (𝜑 → (#‘𝐴) ∈ ℕ0)
196 bcpasc 13148 . . . 4 (((#‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
197195, 1, 196syl2anc 694 . . 3 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
198193, 197eqtr4d 2688 . 2 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))))
199 pm2.1 432 . . . . . . . 8 𝑧𝑥𝑧𝑥)
200199biantrur 526 . . . . . . 7 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾))
201 andir 930 . . . . . . 7 (((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
202200, 201bitri 264 . . . . . 6 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
203202rabbii 3216 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
204 unrab 3931 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
205203, 204eqtr4i 2676 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
206205fveq2i 6232 . . 3 (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
207 ssrab2 3720 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
208 ssfi 8221 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
20959, 207, 208sylancl 695 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
210 inrab 3932 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
211 simprl 809 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → 𝑧𝑥)
212 simpll 805 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
213211, 212pm2.65i 185 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
214213rgenw 2953 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
215 rabeq0 3990 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
216214, 215mpbir 221 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅
217210, 216eqtri 2673 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅
218217a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅)
219 hashun 13209 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅) → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
220209, 62, 218, 219syl3anc 1366 . . 3 (𝜑 → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
221206, 220syl5eq 2697 . 2 (𝜑 → (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
222185, 198, 2213eqtr4d 2695 1 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   class class class wbr 4685  cfv 5926  (class class class)co 6690  cen 7994  Fincfn 7997  cc 9972  1c1 9975   + caddc 9977  cmin 10304  0cn0 11330  cz 11415  Ccbc 13129  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-seq 12842  df-fac 13101  df-bc 13130  df-hash 13158
This theorem is referenced by:  hashbc  13275
  Copyright terms: Public domain W3C validator