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