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

Theorem pwssplit0 26353
 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 2253 . . . . . . 7
3 pwssplit1.b . . . . . . 7
41, 2, 3pwselbasb 13261 . . . . . 6
543adant3 980 . . . . 5
65biimpa 472 . . . 4
7 simpl3 965 . . . 4
8 fssres 5265 . . . 4
96, 7, 8syl2anc 645 . . 3
10 simp1 960 . . . . 5
11 simp3 962 . . . . . 6
12 simp2 961 . . . . . 6
13 ssexg 4057 . . . . . 6
1411, 12, 13syl2anc 645 . . . . 5
15 pwssplit1.z . . . . . 6 s
16 pwssplit1.c . . . . . 6
1715, 2, 16pwselbasb 13261 . . . . 5
1810, 14, 17syl2anc 645 . . . 4