Step |
Hyp |
Ref |
Expression |
1 |
|
pwssplit1.y |
|- Y = ( W ^s U ) |
2 |
|
pwssplit1.z |
|- Z = ( W ^s V ) |
3 |
|
pwssplit1.b |
|- B = ( Base ` Y ) |
4 |
|
pwssplit1.c |
|- C = ( Base ` Z ) |
5 |
|
pwssplit1.f |
|- F = ( x e. B |-> ( x |` V ) ) |
6 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
7 |
1 6 3
|
pwselbasb |
|- ( ( W e. T /\ U e. X ) -> ( x e. B <-> x : U --> ( Base ` W ) ) ) |
8 |
7
|
3adant3 |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> ( x e. B <-> x : U --> ( Base ` W ) ) ) |
9 |
8
|
biimpa |
|- ( ( ( W e. T /\ U e. X /\ V C_ U ) /\ x e. B ) -> x : U --> ( Base ` W ) ) |
10 |
|
simpl3 |
|- ( ( ( W e. T /\ U e. X /\ V C_ U ) /\ x e. B ) -> V C_ U ) |
11 |
9 10
|
fssresd |
|- ( ( ( W e. T /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) : V --> ( Base ` W ) ) |
12 |
|
simp1 |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> W e. T ) |
13 |
|
simp2 |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> U e. X ) |
14 |
|
simp3 |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> V C_ U ) |
15 |
13 14
|
ssexd |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> V e. _V ) |
16 |
2 6 4
|
pwselbasb |
|- ( ( W e. T /\ V e. _V ) -> ( ( x |` V ) e. C <-> ( x |` V ) : V --> ( Base ` W ) ) ) |
17 |
12 15 16
|
syl2anc |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> ( ( x |` V ) e. C <-> ( x |` V ) : V --> ( Base ` W ) ) ) |
18 |
17
|
adantr |
|- ( ( ( W e. T /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( ( x |` V ) e. C <-> ( x |` V ) : V --> ( Base ` W ) ) ) |
19 |
11 18
|
mpbird |
|- ( ( ( W e. T /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) e. C ) |
20 |
19 5
|
fmptd |
|- ( ( W e. T /\ U e. X /\ V C_ U ) -> F : B --> C ) |