Step |
Hyp |
Ref |
Expression |
1 |
|
suppss2f.p |
|- F/ k ph |
2 |
|
suppss2f.a |
|- F/_ k A |
3 |
|
suppss2f.w |
|- F/_ k W |
4 |
|
suppss2f.n |
|- ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) |
5 |
|
suppss2f.v |
|- ( ph -> A e. V ) |
6 |
|
nfcv |
|- F/_ l A |
7 |
|
nfcv |
|- F/_ l B |
8 |
|
nfcsb1v |
|- F/_ k [_ l / k ]_ B |
9 |
|
csbeq1a |
|- ( k = l -> B = [_ l / k ]_ B ) |
10 |
2 6 7 8 9
|
cbvmptf |
|- ( k e. A |-> B ) = ( l e. A |-> [_ l / k ]_ B ) |
11 |
10
|
oveq1i |
|- ( ( k e. A |-> B ) supp Z ) = ( ( l e. A |-> [_ l / k ]_ B ) supp Z ) |
12 |
4
|
sbt |
|- [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) |
13 |
|
sbim |
|- ( [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) <-> ( [ l / k ] ( ph /\ k e. ( A \ W ) ) -> [ l / k ] B = Z ) ) |
14 |
|
sban |
|- ( [ l / k ] ( ph /\ k e. ( A \ W ) ) <-> ( [ l / k ] ph /\ [ l / k ] k e. ( A \ W ) ) ) |
15 |
1
|
sbf |
|- ( [ l / k ] ph <-> ph ) |
16 |
2 3
|
nfdif |
|- F/_ k ( A \ W ) |
17 |
16
|
clelsb3fw |
|- ( [ l / k ] k e. ( A \ W ) <-> l e. ( A \ W ) ) |
18 |
15 17
|
anbi12i |
|- ( ( [ l / k ] ph /\ [ l / k ] k e. ( A \ W ) ) <-> ( ph /\ l e. ( A \ W ) ) ) |
19 |
14 18
|
bitri |
|- ( [ l / k ] ( ph /\ k e. ( A \ W ) ) <-> ( ph /\ l e. ( A \ W ) ) ) |
20 |
|
sbsbc |
|- ( [ l / k ] B = Z <-> [. l / k ]. B = Z ) |
21 |
|
sbceq1g |
|- ( l e. _V -> ( [. l / k ]. B = Z <-> [_ l / k ]_ B = Z ) ) |
22 |
21
|
elv |
|- ( [. l / k ]. B = Z <-> [_ l / k ]_ B = Z ) |
23 |
20 22
|
bitri |
|- ( [ l / k ] B = Z <-> [_ l / k ]_ B = Z ) |
24 |
19 23
|
imbi12i |
|- ( ( [ l / k ] ( ph /\ k e. ( A \ W ) ) -> [ l / k ] B = Z ) <-> ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z ) ) |
25 |
13 24
|
bitri |
|- ( [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) <-> ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z ) ) |
26 |
12 25
|
mpbi |
|- ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z ) |
27 |
26 5
|
suppss2 |
|- ( ph -> ( ( l e. A |-> [_ l / k ]_ B ) supp Z ) C_ W ) |
28 |
11 27
|
eqsstrid |
|- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W ) |