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