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

Theorem hashbclem 13174
Description: Lemma for hashbc 13175: 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 6612 . . . . . . 7 (𝑗 = 𝐾 → ((#‘𝐴)C𝑗) = ((#‘𝐴)C𝐾))
4 eqeq2 2632 . . . . . . . . 9 (𝑗 = 𝐾 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = 𝐾))
54rabbidv 3177 . . . . . . . 8 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})
65fveq2d 6152 . . . . . . 7 (𝑗 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
73, 6eqeq12d 2636 . . . . . 6 (𝑗 = 𝐾 → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
87rspcv 3291 . . . . 5 (𝐾 ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
91, 2, 8sylc 65 . . . 4 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
10 ssun1 3754 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
11 sspwb 4878 . . . . . . . . . . . . 13 (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
1210, 11mpbi 220 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1312sseli 3579 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1413adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
15 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
16 elpwi 4140 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1716ssneld 3585 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1815, 17mpan9 486 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1914, 18jca 554 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
20 elpwi 4140 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
21 uncom 3735 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2220, 21syl6sseq 3630 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2322adantr 481 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
24 simpr 477 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
25 disjsn 4216 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2624, 25sylibr 224 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
27 disjssun 4008 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2826, 27syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2923, 28mpbid 222 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
30 vex 3189 . . . . . . . . . . . 12 𝑥 ∈ V
3130elpw 4136 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3229, 31sylibr 224 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3332adantl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3419, 33impbida 876 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3534anbi1d 740 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾)))
36 anass 680 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
3735, 36syl6bb 276 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾))))
3837rabbidva2 3174 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
3938fveq2d 6152 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
409, 39eqtrd 2655 . . 3 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
41 peano2zm 11364 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
421, 41syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
43 oveq2 6612 . . . . . . 7 (𝑗 = (𝐾 − 1) → ((#‘𝐴)C𝑗) = ((#‘𝐴)C(𝐾 − 1)))
44 eqeq2 2632 . . . . . . . . 9 (𝑗 = (𝐾 − 1) → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = (𝐾 − 1)))
4544rabbidv 3177 . . . . . . . 8 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
4645fveq2d 6152 . . . . . . 7 (𝑗 = (𝐾 − 1) → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
4743, 46eqeq12d 2636 . . . . . 6 (𝑗 = (𝐾 − 1) → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4847rspcv 3291 . . . . 5 ((𝐾 − 1) ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4942, 2, 48sylc 65 . . . 4 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
50 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
51 pwfi 8205 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
5250, 51sylib 208 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
53 rabexg 4772 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
5452, 53syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
55 snfi 7982 . . . . . . . . . 10 {𝑧} ∈ Fin
56 unfi 8171 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5750, 55, 56sylancl 693 . . . . . . . . 9 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
58 pwfi 8205 . . . . . . . . 9 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5957, 58sylib 208 . . . . . . . 8 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
60 ssrab2 3666 . . . . . . . 8 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
61 ssfi 8124 . . . . . . . 8 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
6259, 60, 61sylancl 693 . . . . . . 7 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
63 elex 3198 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
6462, 63syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
65 fveq2 6148 . . . . . . . . 9 (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
6665eqeq1d 2623 . . . . . . . 8 (𝑥 = 𝑢 → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘𝑢) = (𝐾 − 1)))
6766elrab 3346 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)))
68 elpwi 4140 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6968ad2antrl 763 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
70 unss1 3760 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7169, 70syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
72 vex 3189 . . . . . . . . . . . 12 𝑢 ∈ V
73 snex 4869 . . . . . . . . . . . 12 {𝑧} ∈ V
7472, 73unex 6909 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7574elpw 4136 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7671, 75sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7750adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
78 ssfi 8124 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑢𝐴) → 𝑢 ∈ Fin)
7977, 69, 78syl2anc 692 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
8055a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
8115adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
8269, 81ssneldd 3586 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
83 disjsn 4216 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8482, 83sylibr 224 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
85 hashun 13111 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
8679, 80, 84, 85syl3anc 1323 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
87 simprr 795 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘𝑢) = (𝐾 − 1))
88 vex 3189 . . . . . . . . . . . . . 14 𝑧 ∈ V
89 hashsng 13099 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (#‘{𝑧}) = 1)
9088, 89ax-mp 5 . . . . . . . . . . . . 13 (#‘{𝑧}) = 1
9190a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘{𝑧}) = 1)
9287, 91oveq12d 6622 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((#‘𝑢) + (#‘{𝑧})) = ((𝐾 − 1) + 1))
931adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
9493zcnd 11427 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
95 ax-1cn 9938 . . . . . . . . . . . 12 1 ∈ ℂ
96 npcan 10234 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9794, 95, 96sylancl 693 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9886, 92, 973eqtrd 2659 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = 𝐾)
99 ssun2 3755 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
10088snss 4286 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
10199, 100mpbir 221 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
10298, 101jctil 559 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
103 eleq2 2687 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
104 fveq2 6148 . . . . . . . . . . . 12 (𝑥 = (𝑢 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑧})))
105104eqeq1d 2623 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
106103, 105anbi12d 746 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
107106elrab 3346 . . . . . . . . 9 ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
10876, 102, 107sylanbrc 697 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
109108ex 450 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
11067, 109syl5bi 232 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
111 eleq2 2687 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
112 fveq2 6148 . . . . . . . . . 10 (𝑥 = 𝑣 → (#‘𝑥) = (#‘𝑣))
113112eqeq1d 2623 . . . . . . . . 9 (𝑥 = 𝑣 → ((#‘𝑥) = 𝐾 ↔ (#‘𝑣) = 𝐾))
114111, 113anbi12d 746 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
115114elrab 3346 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
116 elpwi 4140 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
117116ad2antrl 763 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
118117, 21syl6sseq 3630 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
119 ssundif 4024 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
120118, 119sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
121 vex 3189 . . . . . . . . . . . 12 𝑣 ∈ V
122 difexg 4768 . . . . . . . . . . . 12 (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V)
123121, 122ax-mp 5 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
124123elpw 4136 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
125120, 124sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
12650adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
127 ssfi 8124 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin)
128126, 120, 127syl2anc 692 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
129 hashcl 13087 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
130128, 129syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
131130nn0cnd 11297 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℂ)
132 pncan 10231 . . . . . . . . . . 11 (((#‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
133131, 95, 132sylancl 693 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
134 undif1 4015 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
135 simprrl 803 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
136135snssd 4309 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
137 ssequn2 3764 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
138136, 137sylib 208 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
139134, 138syl5eq 2667 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
140139fveq2d 6152 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (#‘𝑣))
14155a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
142 incom 3783 . . . . . . . . . . . . . . . 16 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
143 disjdif 4012 . . . . . . . . . . . . . . . 16 ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
144142, 143eqtri 2643 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
145144a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
146 hashun 13111 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
147128, 141, 145, 146syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
14890oveq2i 6615 . . . . . . . . . . . . 13 ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1)
149147, 148syl6eq 2671 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1))
150 simprrr 804 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘𝑣) = 𝐾)
151140, 149, 1503eqtr3d 2663 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((#‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
152151oveq1d 6619 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
153133, 152eqtr3d 2657 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
154 fveq2 6148 . . . . . . . . . . 11 (𝑥 = (𝑣 ∖ {𝑧}) → (#‘𝑥) = (#‘(𝑣 ∖ {𝑧})))
155154eqeq1d 2623 . . . . . . . . . 10 (𝑥 = (𝑣 ∖ {𝑧}) → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
156155elrab 3346 . . . . . . . . 9 ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
157125, 153, 156sylanbrc 697 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
158157ex 450 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
159115, 158syl5bi 232 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
16067, 115anbi12i 732 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))))
161 simp3rl 1132 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
162161snssd 4309 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
163 incom 3783 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
164843adant3 1079 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
165163, 164syl5eq 2667 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
166 uneqdifeq 4029 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
167162, 165, 166syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
168167bicomd 213 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
169 eqcom 2628 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
170 eqcom 2628 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
171 uncom 3735 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
172171eqeq1i 2626 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
173170, 172bitri 264 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
174168, 169, 1733bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1751743expib 1265 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
176160, 175syl5bi 232 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
17754, 64, 110, 159, 176en3d 7936 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
178 ssrab2 3666 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
179 ssfi 8124 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
18052, 178, 179sylancl 693 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
181 hashen 13075 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin) → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
182180, 62, 181syl2anc 692 . . . . 5 (𝜑 → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
183177, 182mpbird 247 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18449, 183eqtrd 2655 . . 3 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18540, 184oveq12d 6622 . 2 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
18655a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
187 disjsn 4216 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
18815, 187sylibr 224 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
189 hashun 13111 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19050, 186, 188, 189syl3anc 1323 . . . . 5 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19190oveq2i 6615 . . . . 5 ((#‘𝐴) + (#‘{𝑧})) = ((#‘𝐴) + 1)
192190, 191syl6eq 2671 . . . 4 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + 1))
193192oveq1d 6619 . . 3 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴) + 1)C𝐾))
194 hashcl 13087 . . . . 5 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
19550, 194syl 17 . . . 4 (𝜑 → (#‘𝐴) ∈ ℕ0)
196 bcpasc 13048 . . . 4 (((#‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
197195, 1, 196syl2anc 692 . . 3 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
198193, 197eqtr4d 2658 . 2 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))))
199 pm2.1 433 . . . . . . . . 9 𝑧𝑥𝑧𝑥)
200199biantrur 527 . . . . . . . 8 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾))
201 andir 911 . . . . . . . 8 (((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
202200, 201bitri 264 . . . . . . 7 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
203202a1i 11 . . . . . 6 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))))
204203rabbiia 3173 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
205 unrab 3874 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
206204, 205eqtr4i 2646 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
207206fveq2i 6151 . . 3 (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
208 ssrab2 3666 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
209 ssfi 8124 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
21059, 208, 209sylancl 693 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
211 inrab 3875 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
212 simprl 793 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → 𝑧𝑥)
213 simpll 789 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
214212, 213pm2.65i 185 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
215214rgenw 2919 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
216 rabeq0 3931 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
217215, 216mpbir 221 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅
218211, 217eqtri 2643 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅
219218a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅)
220 hashun 13111 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅) → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
221210, 62, 219, 220syl3anc 1323 . . 3 (𝜑 → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
222207, 221syl5eq 2667 . 2 (𝜑 → (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
223185, 198, 2223eqtr4d 2665 1 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  {crab 2911  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   class class class wbr 4613  cfv 5847  (class class class)co 6604  cen 7896  Fincfn 7899  cc 9878  1c1 9881   + caddc 9883  cmin 10210  0cn0 11236  cz 11321  Ccbc 13029  #chash 13057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-n0 11237  df-z 11322  df-uz 11632  df-rp 11777  df-fz 12269  df-seq 12742  df-fac 13001  df-bc 13030  df-hash 13058
This theorem is referenced by:  hashbc  13175
  Copyright terms: Public domain W3C validator