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 } ) ) |