Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwssplit0 Structured version   Unicode version

Theorem pwssplit0 17916
 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 2402 . . . . . . 7
3 pwssplit1.b . . . . . . 7
41, 2, 3pwselbasb 14994 . . . . . 6
543adant3 1017 . . . . 5
65biimpa 482 . . . 4
7 simpl3 1002 . . . 4
86, 7fssresd 5691 . . 3
9 simp1 997 . . . . 5
10 simp2 998 . . . . . 6
11 simp3 999 . . . . . 6
1210, 11ssexd 4540 . . . . 5
13 pwssplit1.z . . . . . 6 s
14 pwssplit1.c . . . . . 6
1513, 2, 14pwselbasb 14994 . . . . 5
169, 12, 15syl2anc 659 . . . 4