Metamath Proof Explorer


Theorem hashbclem

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

Ref Expression
Hypotheses hashbc.1
|- ( ph -> A e. Fin )
hashbc.2
|- ( ph -> -. z e. A )
hashbc.3
|- ( ph -> A. j e. ZZ ( ( # ` A ) _C j ) = ( # ` { x e. ~P A | ( # ` x ) = j } ) )
hashbc.4
|- ( ph -> K e. ZZ )
Assertion hashbclem
|- ( ph -> ( ( # ` ( A u. { z } ) ) _C K ) = ( # ` { x e. ~P ( A u. { z } ) | ( # ` x ) = K } ) )

Proof

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