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

Theorem hashbclem 14349
Description: Lemma for hashbc 14350: 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 7365 . . . . . 6 (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾))
2 eqeq2 2748 . . . . . . . 8 (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾))
32rabbidv 3415 . . . . . . 7 (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})
43fveq2d 6846 . . . . . 6 (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
51, 4eqeq12d 2752 . . . . 5 (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})))
6 hashbc.3 . . . . 5 (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))
7 hashbc.4 . . . . 5 (𝜑𝐾 ∈ ℤ)
85, 6, 7rspcdva 3582 . . . 4 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))
9 ssun1 4132 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑧})
109sspwi 4572 . . . . . . . . . . . 12 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
1110sseli 3940 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
1211adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
13 hashbc.2 . . . . . . . . . . 11 (𝜑 → ¬ 𝑧𝐴)
14 elpwi 4567 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
1514ssneld 3946 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧𝐴 → ¬ 𝑧𝑥))
1613, 15mpan9 507 . . . . . . . . . 10 ((𝜑𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧𝑥)
1712, 16jca 512 . . . . . . . . 9 ((𝜑𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥))
18 elpwi 4567 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
19 uncom 4113 . . . . . . . . . . . . . 14 (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
2018, 19sseqtrdi 3994 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
2120adantr 481 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
22 simpr 485 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → ¬ 𝑧𝑥)
23 disjsn 4672 . . . . . . . . . . . . . 14 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
2422, 23sylibr 233 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ∩ {𝑧}) = ∅)
25 disjssun 4427 . . . . . . . . . . . . 13 ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2624, 25syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥𝐴))
2721, 26mpbid 231 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥𝐴)
28 vex 3449 . . . . . . . . . . . 12 𝑥 ∈ V
2928elpw 4564 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3027, 29sylibr 233 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) → 𝑥 ∈ 𝒫 𝐴)
3130adantl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)) → 𝑥 ∈ 𝒫 𝐴)
3217, 31impbida 799 . . . . . . . 8 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥)))
3332anbi1d 630 . . . . . . 7 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾)))
34 anass 469 . . . . . . 7 (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
3533, 34bitrdi 286 . . . . . 6 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))))
3635rabbidva2 3409 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
3736fveq2d 6846 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
388, 37eqtrd 2776 . . 3 (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
39 oveq2 7365 . . . . . 6 (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1)))
40 eqeq2 2748 . . . . . . . 8 (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1)))
4140rabbidv 3415 . . . . . . 7 (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
4241fveq2d 6846 . . . . . 6 (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
4339, 42eqeq12d 2752 . . . . 5 (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})))
44 peano2zm 12546 . . . . . 6 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
457, 44syl 17 . . . . 5 (𝜑 → (𝐾 − 1) ∈ ℤ)
4643, 6, 45rspcdva 3582 . . . 4 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
47 hashbc.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
48 pwfi 9122 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
4947, 48sylib 217 . . . . . . 7 (𝜑 → 𝒫 𝐴 ∈ Fin)
50 rabexg 5288 . . . . . . 7 (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
5149, 50syl 17 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V)
52 snfi 8988 . . . . . . . . 9 {𝑧} ∈ Fin
53 unfi 9116 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
5447, 52, 53sylancl 586 . . . . . . . 8 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
55 pwfi 9122 . . . . . . . 8 ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
5654, 55sylib 217 . . . . . . 7 (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
57 ssrab2 4037 . . . . . . 7 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
58 ssfi 9117 . . . . . . 7 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
5956, 57, 58sylancl 586 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
60 fveqeq2 6851 . . . . . . . 8 (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1)))
6160elrab 3645 . . . . . . 7 (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)))
62 eleq2 2826 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧𝑥𝑧 ∈ (𝑢 ∪ {𝑧})))
63 fveqeq2 6851 . . . . . . . . . 10 (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
6462, 63anbi12d 631 . . . . . . . . 9 (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)))
65 elpwi 4567 . . . . . . . . . . . 12 (𝑢 ∈ 𝒫 𝐴𝑢𝐴)
6665ad2antrl 726 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢𝐴)
67 unss1 4139 . . . . . . . . . . 11 (𝑢𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
6866, 67syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
69 vex 3449 . . . . . . . . . . . 12 𝑢 ∈ V
70 vsnex 5386 . . . . . . . . . . . 12 {𝑧} ∈ V
7169, 70unex 7680 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) ∈ V
7271elpw 4564 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
7368, 72sylibr 233 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
7447adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
7574, 66ssfid 9211 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
7652a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
7713adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝐴)
7866, 77ssneldd 3947 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧𝑢)
79 disjsn 4672 . . . . . . . . . . . . 13 ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑢)
8078, 79sylibr 233 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
81 hashun 14282 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
8275, 76, 80, 81syl3anc 1371 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧})))
83 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1))
84 hashsng 14269 . . . . . . . . . . . . . 14 (𝑧 ∈ V → (♯‘{𝑧}) = 1)
8584elv 3451 . . . . . . . . . . . . 13 (♯‘{𝑧}) = 1
8685a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1)
8783, 86oveq12d 7375 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1))
887adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
8988zcnd 12608 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
90 ax-1cn 11109 . . . . . . . . . . . 12 1 ∈ ℂ
91 npcan 11410 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9289, 90, 91sylancl 586 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9382, 87, 923eqtrd 2780 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾)
94 ssun2 4133 . . . . . . . . . . 11 {𝑧} ⊆ (𝑢 ∪ {𝑧})
95 vex 3449 . . . . . . . . . . . 12 𝑧 ∈ V
9695snss 4746 . . . . . . . . . . 11 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
9794, 96mpbir 230 . . . . . . . . . 10 𝑧 ∈ (𝑢 ∪ {𝑧})
9893, 97jctil 520 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))
9964, 73, 98elrabd 3647 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
10099ex 413 . . . . . . 7 (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
10161, 100biimtrid 241 . . . . . 6 (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
102 eleq2 2826 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑧𝑥𝑧𝑣))
103 fveqeq2 6851 . . . . . . . . 9 (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾))
104102, 103anbi12d 631 . . . . . . . 8 (𝑥 = 𝑣 → ((𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
105104elrab 3645 . . . . . . 7 (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)))
106 fveqeq2 6851 . . . . . . . . 9 (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
107 elpwi 4567 . . . . . . . . . . . . 13 (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
108107ad2antrl 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
109108, 19sseqtrdi 3994 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
110 ssundif 4445 . . . . . . . . . . 11 (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
111109, 110sylib 217 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
112 vex 3449 . . . . . . . . . . . 12 𝑣 ∈ V
113112difexi 5285 . . . . . . . . . . 11 (𝑣 ∖ {𝑧}) ∈ V
114113elpw 4564 . . . . . . . . . 10 ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
115111, 114sylibr 233 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
11647adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
117116, 111ssfid 9211 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
118 hashcl 14256 . . . . . . . . . . . . 13 ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
119117, 118syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℕ0)
120119nn0cnd 12475 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ)
121 pncan 11407 . . . . . . . . . . 11 (((♯‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
122120, 90, 121sylancl 586 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧})))
123 undif1 4435 . . . . . . . . . . . . . 14 ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
124 simprrl 779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
125124snssd 4769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
126 ssequn2 4143 . . . . . . . . . . . . . . 15 ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
127125, 126sylib 217 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
128123, 127eqtrid 2788 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
129128fveq2d 6846 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣))
13052a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
131 disjdifr 4432 . . . . . . . . . . . . . . 15 ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
132131a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
133 hashun 14282 . . . . . . . . . . . . . 14 (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
134117, 130, 132, 133syl3anc 1371 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})))
13585oveq2i 7368 . . . . . . . . . . . . 13 ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)
136134, 135eqtrdi 2792 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1))
137 simprrr 780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾)
138129, 136, 1373eqtr3d 2784 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
139138oveq1d 7372 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
140122, 139eqtr3d 2778 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
141106, 115, 140elrabd 3647 . . . . . . . 8 ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})
142141ex 413 . . . . . . 7 (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
143105, 142biimtrid 241 . . . . . 6 (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))
14461, 105anbi12i 627 . . . . . . 7 ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))))
145 simp3rl 1246 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧𝑣)
146145snssd 4769 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
147 incom 4161 . . . . . . . . . . . 12 ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
148803adant3 1132 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
149147, 148eqtrid 2788 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
150 uneqdifeq 4450 . . . . . . . . . . 11 (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
151146, 149, 150syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
152151bicomd 222 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
153 eqcom 2743 . . . . . . . . 9 (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
154 eqcom 2743 . . . . . . . . . 10 (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
155 uncom 4113 . . . . . . . . . . 11 (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
156155eqeq1i 2741 . . . . . . . . . 10 ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
157154, 156bitri 274 . . . . . . . . 9 (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
158152, 153, 1573bitr4g 313 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
1591583expib 1122 . . . . . . 7 (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
160144, 159biimtrid 241 . . . . . 6 (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
16151, 59, 101, 143, 160en3d 8929 . . . . 5 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
162 ssrab2 4037 . . . . . . 7 {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
163 ssfi 9117 . . . . . . 7 ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
16449, 162, 163sylancl 586 . . . . . 6 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin)
165 hashen 14247 . . . . . 6 (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
166164, 59, 165syl2anc 584 . . . . 5 (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
167161, 166mpbird 256 . . . 4 (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
16846, 167eqtrd 2776 . . 3 (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
16938, 168oveq12d 7375 . 2 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
17052a1i 11 . . . . . 6 (𝜑 → {𝑧} ∈ Fin)
171 disjsn 4672 . . . . . . 7 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
17213, 171sylibr 233 . . . . . 6 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
173 hashun 14282 . . . . . 6 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17447, 170, 172, 173syl3anc 1371 . . . . 5 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧})))
17585oveq2i 7368 . . . . 5 ((♯‘𝐴) + (♯‘{𝑧})) = ((♯‘𝐴) + 1)
176174, 175eqtrdi 2792 . . . 4 (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1))
177176oveq1d 7372 . . 3 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾))
178 hashcl 14256 . . . . 5 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
17947, 178syl 17 . . . 4 (𝜑 → (♯‘𝐴) ∈ ℕ0)
180 bcpasc 14221 . . . 4 (((♯‘𝐴) ∈ ℕ0𝐾 ∈ ℤ) → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
181179, 7, 180syl2anc 584 . . 3 (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾))
182177, 181eqtr4d 2779 . 2 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))))
183 pm2.1 895 . . . . . . . 8 𝑧𝑥𝑧𝑥)
184183biantrur 531 . . . . . . 7 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾))
185 andir 1007 . . . . . . 7 (((¬ 𝑧𝑥𝑧𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
186184, 185bitri 274 . . . . . 6 ((♯‘𝑥) = 𝐾 ↔ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
187186rabbii 3413 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
188 unrab 4265 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
189187, 188eqtr4i 2767 . . . 4 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})
190189fveq2i 6845 . . 3 (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}))
191 ssrab2 4037 . . . . 5 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
192 ssfi 9117 . . . . 5 ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
19356, 191, 192sylancl 586 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin)
194 inrab 4266 . . . . . 6 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))}
195 simprl 769 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧𝑥)
196 simpll 765 . . . . . . . . 9 (((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧𝑥)
197195, 196pm2.65i 193 . . . . . . . 8 ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
198197rgenw 3068 . . . . . . 7 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))
199 rabeq0 4344 . . . . . . 7 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)))
200198, 199mpbir 230 . . . . . 6 {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅
201194, 200eqtri 2764 . . . . 5 ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅
202201a1i 11 . . . 4 (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅)
203 hashun 14282 . . . 4 (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
204193, 59, 202, 203syl3anc 1371 . . 3 (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
205190, 204eqtrid 2788 . 2 (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧𝑥 ∧ (♯‘𝑥) = 𝐾)})))
206169, 182, 2053eqtr4d 2786 1 (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105  cfv 6496  (class class class)co 7357  cen 8880  Fincfn 8883  cc 11049  1c1 11052   + caddc 11054  cmin 11385  0cn0 12413  cz 12499  Ccbc 14202  chash 14230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-seq 13907  df-fac 14174  df-bc 14203  df-hash 14231
This theorem is referenced by:  hashbc  14350
  Copyright terms: Public domain W3C validator