Metamath Proof Explorer

Theorem hashbclem

Description: Lemma for hashbc : inductive step. (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Hypotheses hashbc.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
hashbc.2 ⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐴 )
hashbc.3 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℤ ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) )
hashbc.4 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
Assertion hashbclem ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )

Proof

Step Hyp Ref Expression
1 hashbc.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 hashbc.2 ⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐴 )
3 hashbc.3 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℤ ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) )
4 hashbc.4 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5 oveq2 ⊢ ( 𝑗 = 𝐾 → ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ( ♯ ‘ 𝐴 ) C 𝐾 ) )
6 eqeq2 ⊢ ( 𝑗 = 𝐾 → ( ( ♯ ‘ 𝑥 ) = 𝑗 ↔ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
7 6 rabbidv ⊢ ( 𝑗 = 𝐾 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } )
8 7 fveq2d ⊢ ( 𝑗 = 𝐾 → ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )
9 5 8 eqeq12d ⊢ ( 𝑗 = 𝐾 → ( ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) ↔ ( ( ♯ ‘ 𝐴 ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) ) )
10 9 3 4 rspcdva ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )
11 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑧 } )
12 11 sspwi ⊢ 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } )
13 12 sseli ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) )
15 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
16 15 ssneld ⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥 ) )
17 2 16 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ¬ 𝑧 ∈ 𝑥 )
18 14 17 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) )
19 elpwi ⊢ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) → 𝑥 ⊆ ( 𝐴 ∪ { 𝑧 } ) )
20 uncom ⊢ ( 𝐴 ∪ { 𝑧 } ) = ( { 𝑧 } ∪ 𝐴 )
21 19 20 sseqtrdi ⊢ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) → 𝑥 ⊆ ( { 𝑧 } ∪ 𝐴 ) )
22 21 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → 𝑥 ⊆ ( { 𝑧 } ∪ 𝐴 ) )
23 simpr ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → ¬ 𝑧 ∈ 𝑥 )
24 disjsn ⊢ ( ( 𝑥 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑥 )
25 23 24 sylibr ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝑥 ∩ { 𝑧 } ) = ∅ )
26 disjssun ⊢ ( ( 𝑥 ∩ { 𝑧 } ) = ∅ → ( 𝑥 ⊆ ( { 𝑧 } ∪ 𝐴 ) ↔ 𝑥 ⊆ 𝐴 ) )
27 25 26 syl ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝑥 ⊆ ( { 𝑧 } ∪ 𝐴 ) ↔ 𝑥 ⊆ 𝐴 ) )
28 22 27 mpbid ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → 𝑥 ⊆ 𝐴 )
29 vex ⊢ 𝑥 ∈ V
30 29 elpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
31 28 30 sylibr ⊢ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
32 31 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) ) → 𝑥 ∈ 𝒫 𝐴 )
33 18 32 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 ↔ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) ) )
34 33 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
35 anass ⊢ ( ( ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
36 34 35 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) ) )
37 36 rabbidva2 ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
38 37 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
39 10 38 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
40 oveq2 ⊢ ( 𝑗 = ( 𝐾 − 1 ) → ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) )
41 eqeq2 ⊢ ( 𝑗 = ( 𝐾 − 1 ) → ( ( ♯ ‘ 𝑥 ) = 𝑗 ↔ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) ) )
42 41 rabbidv ⊢ ( 𝑗 = ( 𝐾 − 1 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } )
43 42 fveq2d ⊢ ( 𝑗 = ( 𝐾 − 1 ) → ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
44 40 43 eqeq12d ⊢ ( 𝑗 = ( 𝐾 − 1 ) → ( ( ( ♯ ‘ 𝐴 ) C 𝑗 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑗 } ) ↔ ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) ) )
45 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
46 4 45 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℤ )
47 44 3 46 rspcdva ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
48 pwfi ⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
49 1 48 sylib ⊢ ( 𝜑 → 𝒫 𝐴 ∈ Fin )
50 rabexg ⊢ ( 𝒫 𝐴 ∈ Fin → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ V )
51 49 50 syl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ V )
52 snfi ⊢ { 𝑧 } ∈ Fin
53 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
54 1 52 53 sylancl ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
55 pwfi ⊢ ( ( 𝐴 ∪ { 𝑧 } ) ∈ Fin ↔ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
56 54 55 sylib ⊢ ( 𝜑 → 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∈ Fin )
57 ssrab2 ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } )
58 ssfi ⊢ ( ( 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ) → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
59 56 57 58 sylancl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
60 fveqeq2 ⊢ ( 𝑥 = 𝑢 → ( ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) ↔ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) )
61 60 elrab ⊢ ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ↔ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) )
62 eleq2 ⊢ ( 𝑥 = ( 𝑢 ∪ { 𝑧 } ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) ) )
63 fveqeq2 ⊢ ( 𝑥 = ( 𝑢 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = 𝐾 ) )
64 62 63 anbi12d ⊢ ( 𝑥 = ( 𝑢 ∪ { 𝑧 } ) → ( ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) ∧ ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = 𝐾 ) ) )
65 elpwi ⊢ ( 𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴 )
66 65 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → 𝑢 ⊆ 𝐴 )
67 unss1 ⊢ ( 𝑢 ⊆ 𝐴 → ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝐴 ∪ { 𝑧 } ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝐴 ∪ { 𝑧 } ) )
69 vex ⊢ 𝑢 ∈ V
70 snex ⊢ { 𝑧 } ∈ V
71 69 70 unex ⊢ ( 𝑢 ∪ { 𝑧 } ) ∈ V
72 71 elpw ⊢ ( ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ↔ ( 𝑢 ∪ { 𝑧 } ) ⊆ ( 𝐴 ∪ { 𝑧 } ) )
73 68 72 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( 𝑢 ∪ { 𝑧 } ) ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) )
74 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → 𝐴 ∈ Fin )
75 74 66 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → 𝑢 ∈ Fin )
76 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → { 𝑧 } ∈ Fin )
77 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ¬ 𝑧 ∈ 𝐴 )
78 66 77 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ¬ 𝑧 ∈ 𝑢 )
79 disjsn ⊢ ( ( 𝑢 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑢 )
80 78 79 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( 𝑢 ∩ { 𝑧 } ) = ∅ )
81 hashun ⊢ ( ( 𝑢 ∈ Fin ∧ { 𝑧 } ∈ Fin ∧ ( 𝑢 ∩ { 𝑧 } ) = ∅ ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑢 ) + ( ♯ ‘ { 𝑧 } ) ) )
82 75 76 80 81 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑢 ) + ( ♯ ‘ { 𝑧 } ) ) )
83 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) )
84 hashsng ⊢ ( 𝑧 ∈ V → ( ♯ ‘ { 𝑧 } ) = 1 )
85 84 elv ⊢ ( ♯ ‘ { 𝑧 } ) = 1
86 85 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ♯ ‘ { 𝑧 } ) = 1 )
87 83 86 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ 𝑢 ) + ( ♯ ‘ { 𝑧 } ) ) = ( ( 𝐾 − 1 ) + 1 ) )
88 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
89 88 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℂ )
90 ax-1cn ⊢ 1 ∈ ℂ
91 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
92 89 90 91 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
93 82 87 92 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = 𝐾 )
94 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑢 ∪ { 𝑧 } )
95 vex ⊢ 𝑧 ∈ V
96 95 snss ⊢ ( 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) ↔ { 𝑧 } ⊆ ( 𝑢 ∪ { 𝑧 } ) )
97 94 96 mpbir ⊢ 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } )
98 93 97 jctil ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( 𝑧 ∈ ( 𝑢 ∪ { 𝑧 } ) ∧ ( ♯ ‘ ( 𝑢 ∪ { 𝑧 } ) ) = 𝐾 ) )
99 64 73 98 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ) → ( 𝑢 ∪ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
100 99 ex ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) → ( 𝑢 ∪ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
101 61 100 syl5bi ⊢ ( 𝜑 → ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } → ( 𝑢 ∪ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
102 eleq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣 ) )
103 fveqeq2 ⊢ ( 𝑥 = 𝑣 → ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ♯ ‘ 𝑣 ) = 𝐾 ) )
104 102 103 anbi12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) )
105 104 elrab ⊢ ( 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ↔ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) )
106 fveqeq2 ⊢ ( 𝑥 = ( 𝑣 ∖ { 𝑧 } ) → ( ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) ↔ ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) = ( 𝐾 − 1 ) ) )
107 elpwi ⊢ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) → 𝑣 ⊆ ( 𝐴 ∪ { 𝑧 } ) )
108 107 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝑣 ⊆ ( 𝐴 ∪ { 𝑧 } ) )
109 108 20 sseqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝑣 ⊆ ( { 𝑧 } ∪ 𝐴 ) )
110 ssundif ⊢ ( 𝑣 ⊆ ( { 𝑧 } ∪ 𝐴 ) ↔ ( 𝑣 ∖ { 𝑧 } ) ⊆ 𝐴 )
111 109 110 sylib ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∖ { 𝑧 } ) ⊆ 𝐴 )
112 vex ⊢ 𝑣 ∈ V
113 112 difexi ⊢ ( 𝑣 ∖ { 𝑧 } ) ∈ V
114 113 elpw ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∈ 𝒫 𝐴 ↔ ( 𝑣 ∖ { 𝑧 } ) ⊆ 𝐴 )
115 111 114 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ 𝒫 𝐴 )
116 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝐴 ∈ Fin )
117 116 111 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ Fin )
118 hashcl ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∈ Fin → ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) ∈ ℕ0 )
119 117 118 syl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) ∈ ℕ0 )
120 119 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) ∈ ℂ )
121 pncan ⊢ ( ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) − 1 ) = ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) )
122 120 90 121 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) − 1 ) = ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) )
123 undif1 ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( 𝑣 ∪ { 𝑧 } )
124 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝑧 ∈ 𝑣 )
125 124 snssd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → { 𝑧 } ⊆ 𝑣 )
126 ssequn2 ⊢ ( { 𝑧 } ⊆ 𝑣 ↔ ( 𝑣 ∪ { 𝑧 } ) = 𝑣 )
127 125 126 sylib ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∪ { 𝑧 } ) = 𝑣 )
128 123 127 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑣 )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ♯ ‘ 𝑣 ) )
130 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → { 𝑧 } ∈ Fin )
131 disjdifr ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅
132 131 a1i ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ )
133 hashun ⊢ ( ( ( 𝑣 ∖ { 𝑧 } ) ∈ Fin ∧ { 𝑧 } ∈ Fin ∧ ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) )
134 117 130 132 133 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) )
135 85 oveq2i ⊢ ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 )
136 134 135 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) )
137 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ 𝑣 ) = 𝐾 )
138 129 136 137 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) = 𝐾 )
139 138 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) − 1 ) = ( 𝐾 − 1 ) )
140 122 139 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) = ( 𝐾 − 1 ) )
141 106 115 140 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } )
142 141 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
143 105 142 syl5bi ⊢ ( 𝜑 → ( 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
144 61 105 anbi12i ⊢ ( ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∧ 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ ( ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) )
145 simp3rl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝑧 ∈ 𝑣 )
146 145 snssd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → { 𝑧 } ⊆ 𝑣 )
147 incom ⊢ ( { 𝑧 } ∩ 𝑢 ) = ( 𝑢 ∩ { 𝑧 } )
148 80 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 ∩ { 𝑧 } ) = ∅ )
149 147 148 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( { 𝑧 } ∩ 𝑢 ) = ∅ )
150 uneqdifeq ⊢ ( ( { 𝑧 } ⊆ 𝑣 ∧ ( { 𝑧 } ∩ 𝑢 ) = ∅ ) → ( ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ) )
151 146 149 150 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ) )
152 151 bicomd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ) )
153 eqcom ⊢ ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 )
154 eqcom ⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ↔ ( 𝑢 ∪ { 𝑧 } ) = 𝑣 )
155 uncom ⊢ ( 𝑢 ∪ { 𝑧 } ) = ( { 𝑧 } ∪ 𝑢 )
156 155 eqeq1i ⊢ ( ( 𝑢 ∪ { 𝑧 } ) = 𝑣 ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 )
157 154 156 bitri ⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 )
158 152 153 157 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) )
159 158 3expib ⊢ ( 𝜑 → ( ( ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) ) )
160 144 159 syl5bi ⊢ ( 𝜑 → ( ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∧ 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) ) )
161 51 59 101 143 160 en3d ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
162 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ⊆ 𝒫 𝐴
163 ssfi ⊢ ( ( 𝒫 𝐴 ∈ Fin ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ⊆ 𝒫 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin )
164 49 162 163 sylancl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin )
165 hashen ⊢ ( ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ) → ( ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
166 164 59 165 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
167 161 166 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
168 47 167 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
169 39 168 oveq12d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
170 52 a1i ⊢ ( 𝜑 → { 𝑧 } ∈ Fin )
171 disjsn ⊢ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝐴 )
172 2 171 sylibr ⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
173 hashun ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 } ∈ Fin ∧ ( 𝐴 ∩ { 𝑧 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) )
174 1 170 172 173 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) )
175 85 oveq2i ⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 )
176 174 175 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
177 176 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
178 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
179 1 178 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
180 bcpasc ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
181 179 4 180 syl2anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
182 177 181 eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) )
183 pm2.1 ⊢ ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 )
184 183 biantrur ⊢ ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
185 andir ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
186 184 185 bitri ⊢ ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
187 186 rabbii ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
188 unrab ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
189 187 188 eqtr4i ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } = ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
190 189 fveq2i ⊢ ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) = ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
191 ssrab2 ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } )
192 ssfi ⊢ ( ( 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ) → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
193 56 191 192 sylancl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
194 inrab ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
195 simprl ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) → 𝑧 ∈ 𝑥 )
196 simpll ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) → ¬ 𝑧 ∈ 𝑥 )
197 195 196 pm2.65i ⊢ ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
198 197 rgenw ⊢ ∀ 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
199 rabeq0 ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) } = ∅ ↔ ∀ 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
200 198 199 mpbir ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) } = ∅
201 194 200 eqtri ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅
202 201 a1i ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅ )
203 hashun ⊢ ( ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ∧ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
204 193 59 202 203 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
205 190 204 eqtrid ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
206 169 182 205 3eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )