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

Theorem hashbclem 13093
 Description: Lemma for hashbc 13094: 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 6557 . . . . . . 7 (𝑗 = 𝐾 → ((#‘𝐴)C𝑗) = ((#‘𝐴)C𝐾))
4 eqeq2 2621 . . . . . . . . 9 (𝑗 = 𝐾 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = 𝐾))
54rabbidv 3164 . . . . . . . 8 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})
65fveq2d 6107 . . . . . . 7 (𝑗 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
73, 6eqeq12d 2625 . . . . . 6 (𝑗 = 𝐾 → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
87rspcv 3278 . . . . 5 (𝐾 ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
91, 2, 8sylc 63 . . . 4 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
10 ssun1 3738 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
11 sspwb 4844 . . . . . . . . . . . . 13 (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
1210, 11mpbi 219 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1312sseli 3564 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1413adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
15 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
16 elpwi 4117 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1716ssneld 3570 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1815, 17mpan9 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1914, 18jca 553 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
20 elpwi 4117 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
21 uncom 3719 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2220, 21syl6sseq 3614 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2322adantr 480 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
24 simpr 476 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
25 disjsn 4192 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2624, 25sylibr 223 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
27 disjssun 3988 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2826, 27syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2923, 28mpbid 221 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
30 vex 3176 . . . . . . . . . . . 12 𝑥 ∈ V
3130elpw 4114 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3229, 31sylibr 223 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3332adantl 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3419, 33impbida 873 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3534anbi1d 737 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾)))
36 anass 679 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
3735, 36syl6bb 275 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾))))
3837rabbidva2 3162 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
3938fveq2d 6107 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
409, 39eqtrd 2644 . . 3 (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
41 peano2zm 11297 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
421, 41syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
43 oveq2 6557 . . . . . . 7 (𝑗 = (𝐾 − 1) → ((#‘𝐴)C𝑗) = ((#‘𝐴)C(𝐾 − 1)))
44 eqeq2 2621 . . . . . . . . 9 (𝑗 = (𝐾 − 1) → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = (𝐾 − 1)))
4544rabbidv 3164 . . . . . . . 8 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
4645fveq2d 6107 . . . . . . 7 (𝑗 = (𝐾 − 1) → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
4743, 46eqeq12d 2625 . . . . . 6 (𝑗 = (𝐾 − 1) → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4847rspcv 3278 . . . . 5 ((𝐾 − 1) ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
4942, 2, 48sylc 63 . . . 4 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
50 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
51 pwfi 8144 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
5250, 51sylib 207 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
53 rabexg 4739 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
5452, 53syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
55 snfi 7923 . . . . . . . . . 10 {𝑧} ∈ Fin
56 unfi 8112 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5750, 55, 56sylancl 693 . . . . . . . . 9 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
58 pwfi 8144 . . . . . . . . 9 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5957, 58sylib 207 . . . . . . . 8 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
60 ssrab2 3650 . . . . . . . 8 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
61 ssfi 8065 . . . . . . . 8 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
6259, 60, 61sylancl 693 . . . . . . 7 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
63 elex 3185 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
6462, 63syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
65 fveq2 6103 . . . . . . . . 9 (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
6665eqeq1d 2612 . . . . . . . 8 (𝑥 = 𝑢 → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘𝑢) = (𝐾 − 1)))
6766elrab 3331 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)))
68 elpwi 4117 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6968ad2antrl 760 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
70 unss1 3744 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7169, 70syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
72 vex 3176 . . . . . . . . . . . 12 𝑢 ∈ V
73 snex 4835 . . . . . . . . . . . 12 {𝑧} ∈ V
7472, 73unex 6854 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7574elpw 4114 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7671, 75sylibr 223 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7750adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
78 ssfi 8065 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑢𝐴) → 𝑢 ∈ Fin)
7977, 69, 78syl2anc 691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
8055a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
8115adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
8269, 81ssneldd 3571 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
83 disjsn 4192 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8482, 83sylibr 223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
85 hashun 13032 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
8679, 80, 84, 85syl3anc 1318 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
87 simprr 792 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘𝑢) = (𝐾 − 1))
88 vex 3176 . . . . . . . . . . . . . 14 𝑧 ∈ V
89 hashsng 13020 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (#‘{𝑧}) = 1)
9088, 89ax-mp 5 . . . . . . . . . . . . 13 (#‘{𝑧}) = 1
9190a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘{𝑧}) = 1)
9287, 91oveq12d 6567 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((#‘𝑢) + (#‘{𝑧})) = ((𝐾 − 1) + 1))
931adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
9493zcnd 11359 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
95 ax-1cn 9873 . . . . . . . . . . . 12 1 ∈ ℂ
96 npcan 10169 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9794, 95, 96sylancl 693 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9886, 92, 973eqtrd 2648 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = 𝐾)
99 ssun2 3739 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
10088snss 4259 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
10199, 100mpbir 220 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
10298, 101jctil 558 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
103 eleq2 2677 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
104 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = (𝑢 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑧})))
105104eqeq1d 2612 . . . . . . . . . . 11 (𝑥 = (𝑢 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
106103, 105anbi12d 743 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
107106elrab 3331 . . . . . . . . 9 ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
10876, 102, 107sylanbrc 695 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
109108ex 449 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
11067, 109syl5bi 231 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
111 eleq2 2677 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
112 fveq2 6103 . . . . . . . . . 10 (𝑥 = 𝑣 → (#‘𝑥) = (#‘𝑣))
113112eqeq1d 2612 . . . . . . . . 9 (𝑥 = 𝑣 → ((#‘𝑥) = 𝐾 ↔ (#‘𝑣) = 𝐾))
114111, 113anbi12d 743 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
115114elrab 3331 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)))
116 elpwi 4117 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
117116ad2antrl 760 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
118117, 21syl6sseq 3614 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
119 ssundif 4004 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
120118, 119sylib 207 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
121 vex 3176 . . . . . . . . . . . 12 𝑣 ∈ V
122 difexg 4735 . . . . . . . . . . . 12 (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V)
123121, 122ax-mp 5 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
124123elpw 4114 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
125120, 124sylibr 223 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
12650adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
127 ssfi 8065 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin)
128126, 120, 127syl2anc 691 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
129 hashcl 13009 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
130128, 129syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
131130nn0cnd 11230 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℂ)
132 pncan 10166 . . . . . . . . . . 11 (((#‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
133131, 95, 132sylancl 693 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
134 undif1 3995 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
135 simprrl 800 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
136135snssd 4281 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
137 ssequn2 3748 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
138136, 137sylib 207 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
139134, 138syl5eq 2656 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
140139fveq2d 6107 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (#‘𝑣))
14155a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
142 incom 3767 . . . . . . . . . . . . . . . 16 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
143 disjdif 3992 . . . . . . . . . . . . . . . 16 ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
144142, 143eqtri 2632 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
145144a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
146 hashun 13032 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
147128, 141, 145, 146syl3anc 1318 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
14890oveq2i 6560 . . . . . . . . . . . . 13 ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1)
149147, 148syl6eq 2660 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1))
150 simprrr 801 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘𝑣) = 𝐾)
151140, 149, 1503eqtr3d 2652 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((#‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
152151oveq1d 6564 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
153133, 152eqtr3d 2646 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
154 fveq2 6103 . . . . . . . . . . 11 (𝑥 = (𝑣 ∖ {𝑧}) → (#‘𝑥) = (#‘(𝑣 ∖ {𝑧})))
155154eqeq1d 2612 . . . . . . . . . 10 (𝑥 = (𝑣 ∖ {𝑧}) → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
156155elrab 3331 . . . . . . . . 9 ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
157125, 153, 156sylanbrc 695 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
158157ex 449 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
159115, 158syl5bi 231 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
16067, 115anbi12i 729 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))))
161 simp3rl 1127 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧𝑣)
162161snssd 4281 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
163 incom 3767 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
164843adant3 1074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
165163, 164syl5eq 2656 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
166 uneqdifeq 4009 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
167162, 165, 166syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
168167bicomd 212 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
169 eqcom 2617 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
170 eqcom 2617 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
171 uncom 3719 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
172171eqeq1i 2615 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
173170, 172bitri 263 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
174168, 169, 1733bitr4g 302 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1751743expib 1260 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
176160, 175syl5bi 231 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
17754, 64, 110, 159, 176en3d 7878 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
178 ssrab2 3650 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
179 ssfi 8065 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
18052, 178, 179sylancl 693 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
181 hashen 12997 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin) → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
182180, 62, 181syl2anc 691 . . . . 5 (𝜑 → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
183177, 182mpbird 246 . . . 4 (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18449, 183eqtrd 2644 . . 3 (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
18540, 184oveq12d 6567 . 2 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
18655a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
187 disjsn 4192 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
18815, 187sylibr 223 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
189 hashun 13032 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19050, 186, 188, 189syl3anc 1318 . . . . 5 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
19190oveq2i 6560 . . . . 5 ((#‘𝐴) + (#‘{𝑧})) = ((#‘𝐴) + 1)
192190, 191syl6eq 2660 . . . 4 (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + 1))
193192oveq1d 6564 . . 3 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴) + 1)C𝐾))
194 hashcl 13009 . . . . 5 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
19550, 194syl 17 . . . 4 (𝜑 → (#‘𝐴) ∈ ℕ0)
196 bcpasc 12970 . . . 4 (((#‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
197195, 1, 196syl2anc 691 . . 3 (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
198193, 197eqtr4d 2647 . 2 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))))
199 pm2.1 432 . . . . . . . . 9 𝑧𝑥𝑧𝑥)
200199biantrur 526 . . . . . . . 8 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾))
201 andir 908 . . . . . . . 8 (((¬ 𝑧𝑥𝑧𝑥) ∧ (#‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
202200, 201bitri 263 . . . . . . 7 ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
203202a1i 11 . . . . . 6 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))))
204203rabbiia 3161 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
205 unrab 3857 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
206204, 205eqtr4i 2635 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})
207206fveq2i 6106 . . 3 (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}))
208 ssrab2 3650 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
209 ssfi 8065 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
21059, 208, 209sylancl 693 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
211 inrab 3858 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))}
212 simprl 790 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → 𝑧𝑥)
213 simpll 786 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
214212, 213pm2.65i 184 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
215214rgenw 2908 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))
216 rabeq0 3911 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)))
217215, 216mpbir 220 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅
218211, 217eqtri 2632 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅
219218a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅)
220 hashun 13032 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅) → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
221210, 62, 219, 220syl3anc 1318 . . 3 (𝜑 → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
222207, 221syl5eq 2656 . 2 (𝜑 → (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (#‘𝑥) = 𝐾)})))
223185, 198, 2223eqtr4d 2654 1 (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125   class class class wbr 4583  ‘cfv 5804  (class class class)co 6549   ≈ cen 7838  Fincfn 7841  ℂcc 9813  1c1 9816   + caddc 9818   − cmin 10145  ℕ0cn0 11169  ℤcz 11254  Ccbc 12951  #chash 12979 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-seq 12664  df-fac 12923  df-bc 12952  df-hash 12980 This theorem is referenced by:  hashbc  13094
 Copyright terms: Public domain W3C validator