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 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑣 )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ♯ ‘ 𝑣 ) )
130 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → { 𝑧 } ∈ Fin )
131 incom ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ( { 𝑧 } ∩ ( 𝑣 ∖ { 𝑧 } ) )
132 disjdif ⊢ ( { 𝑧 } ∩ ( 𝑣 ∖ { 𝑧 } ) ) = ∅
133 131 132 eqtri ⊢ ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅
134 133 a1i ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ )
135 hashun ⊢ ( ( ( 𝑣 ∖ { 𝑧 } ) ∈ Fin ∧ { 𝑧 } ∈ Fin ∧ ( ( 𝑣 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) )
136 117 130 134 135 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) )
137 85 oveq2i ⊢ ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + ( ♯ ‘ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 )
138 136 137 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( ( 𝑣 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) )
139 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ 𝑣 ) = 𝐾 )
140 129 138 139 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) = 𝐾 )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) + 1 ) − 1 ) = ( 𝐾 − 1 ) )
142 122 141 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ♯ ‘ ( 𝑣 ∖ { 𝑧 } ) ) = ( 𝐾 − 1 ) )
143 106 115 142 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } )
144 143 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
145 105 144 syl5bi ⊢ ( 𝜑 → ( 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } → ( 𝑣 ∖ { 𝑧 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) )
146 61 105 anbi12i ⊢ ( ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∧ 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ ( ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) )
147 simp3rl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → 𝑧 ∈ 𝑣 )
148 147 snssd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → { 𝑧 } ⊆ 𝑣 )
149 incom ⊢ ( { 𝑧 } ∩ 𝑢 ) = ( 𝑢 ∩ { 𝑧 } )
150 80 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 ∩ { 𝑧 } ) = ∅ )
151 149 150 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( { 𝑧 } ∩ 𝑢 ) = ∅ )
152 uneqdifeq ⊢ ( ( { 𝑧 } ⊆ 𝑣 ∧ ( { 𝑧 } ∩ 𝑢 ) = ∅ ) → ( ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ) )
153 148 151 152 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ) )
154 153 bicomd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( ( 𝑣 ∖ { 𝑧 } ) = 𝑢 ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 ) )
155 eqcom ⊢ ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ ( 𝑣 ∖ { 𝑧 } ) = 𝑢 )
156 eqcom ⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ↔ ( 𝑢 ∪ { 𝑧 } ) = 𝑣 )
157 uncom ⊢ ( 𝑢 ∪ { 𝑧 } ) = ( { 𝑧 } ∪ 𝑢 )
158 157 eqeq1i ⊢ ( ( 𝑢 ∪ { 𝑧 } ) = 𝑣 ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 )
159 156 158 bitri ⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ↔ ( { 𝑧 } ∪ 𝑢 ) = 𝑣 )
160 154 155 159 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) )
161 160 3expib ⊢ ( 𝜑 → ( ( ( 𝑢 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑢 ) = ( 𝐾 − 1 ) ) ∧ ( 𝑣 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∧ ( 𝑧 ∈ 𝑣 ∧ ( ♯ ‘ 𝑣 ) = 𝐾 ) ) ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) ) )
162 146 161 syl5bi ⊢ ( 𝜑 → ( ( 𝑢 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∧ 𝑣 ∈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) → ( 𝑢 = ( 𝑣 ∖ { 𝑧 } ) ↔ 𝑣 = ( 𝑢 ∪ { 𝑧 } ) ) ) )
163 51 59 101 145 162 en3d ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
164 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ⊆ 𝒫 𝐴
165 ssfi ⊢ ( ( 𝒫 𝐴 ∈ Fin ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ⊆ 𝒫 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin )
166 49 164 165 sylancl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin )
167 hashen ⊢ ( ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ) → ( ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
168 166 59 167 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ↔ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ≈ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
169 163 168 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = ( 𝐾 − 1 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
170 47 169 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
171 39 170 oveq12d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
172 52 a1i ⊢ ( 𝜑 → { 𝑧 } ∈ Fin )
173 disjsn ⊢ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝐴 )
174 2 173 sylibr ⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
175 hashun ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 } ∈ Fin ∧ ( 𝐴 ∩ { 𝑧 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) )
176 1 172 174 175 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) )
177 85 oveq2i ⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 )
178 176 177 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
179 178 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
180 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
181 1 180 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
182 bcpasc ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
183 181 4 182 syl2anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) = ( ( ( ♯ ‘ 𝐴 ) + 1 ) C 𝐾 ) )
184 179 183 eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ( ( ♯ ‘ 𝐴 ) C 𝐾 ) + ( ( ♯ ‘ 𝐴 ) C ( 𝐾 − 1 ) ) ) )
185 pm2.1 ⊢ ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 )
186 185 biantrur ⊢ ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
187 andir ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
188 186 187 bitri ⊢ ( ( ♯ ‘ 𝑥 ) = 𝐾 ↔ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
189 188 rabbii ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
190 unrab ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∨ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
191 189 190 eqtr4i ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } = ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } )
192 191 fveq2i ⊢ ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) = ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) )
193 ssrab2 ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } )
194 ssfi ⊢ ( ( 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ⊆ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ) → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
195 56 193 194 sylancl ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin )
196 inrab ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) }
197 simprl ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) → 𝑧 ∈ 𝑥 )
198 simpll ⊢ ( ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) → ¬ 𝑧 ∈ 𝑥 )
199 197 198 pm2.65i ⊢ ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
200 199 rgenw ⊢ ∀ 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) )
201 rabeq0 ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) } = ∅ ↔ ∀ 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ¬ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) )
202 200 201 mpbir ⊢ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) ) } = ∅
203 196 202 eqtri ⊢ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅
204 203 a1i ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅ )
205 hashun ⊢ ( ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ∧ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∈ Fin ∧ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∩ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
206 195 59 204 205 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ∪ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
207 192 206 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) = ( ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ¬ 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( 𝑧 ∈ 𝑥 ∧ ( ♯ ‘ 𝑥 ) = 𝐾 ) } ) ) )
208 171 184 207 3eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ { 𝑧 } ) ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 ( 𝐴 ∪ { 𝑧 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )