Theorem pwssplit0

Description: Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwssplit1.y	|- Y = ( W ^s U )
	pwssplit1.z	|- Z = ( W ^s V )
	pwssplit1.b	|- B = ( Base ` Y )
	pwssplit1.c	|- C = ( Base ` Z )
	pwssplit1.f	|- F = ( x e. B |-> ( x |` V ) )
Assertion	pwssplit0	|- ( ( W e. T /\ U e. X /\ V C_ U ) -> F : B --> C )

Proof

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 )