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