This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )