Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pwssplit0 Structured version   Unicode version

Theorem pwssplit0 27166
 Description: Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
Hypotheses
Ref Expression
pwssplit1.y s
pwssplit1.z s
pwssplit1.b
pwssplit1.c
pwssplit1.f
Assertion
Ref Expression
pwssplit0
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem pwssplit0
StepHypRef Expression
1 pwssplit1.y . . . . . . 7 s
2 eqid 2438 . . . . . . 7
3 pwssplit1.b . . . . . . 7
41, 2, 3pwselbasb 13712 . . . . . 6
543adant3 978 . . . . 5
65biimpa 472 . . . 4
7 simpl3 963 . . . 4
8 fssres 5612 . . . 4
96, 7, 8syl2anc 644 . . 3
10 simp1 958 . . . . 5
11 simp2 959 . . . . . 6
12 simp3 960 . . . . . 6
1311, 12ssexd 4352 . . . . 5
14 pwssplit1.z . . . . . 6 s
15 pwssplit1.c . . . . . 6
1614, 2, 15pwselbasb 13712 . . . . 5
1710, 13, 16syl2anc 644 . . . 4