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

Theorem restco 17220
 Description: Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
Assertion
Ref Expression
restco t t t

Proof of Theorem restco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2951 . . . . 5
21inex1 4336 . . . 4
3 ineq1 3527 . . . . 5
4 inass 3543 . . . . 5
53, 4syl6eq 2483 . . . 4
62, 5abrexco 5978 . . 3
7 eqid 2435 . . . . . 6
87rnmpt 5108 . . . . 5
9 mpteq1 4281 . . . . 5
108, 9ax-mp 8 . . . 4
1110rnmpt 5108 . . 3
12 eqid 2435 . . . 4
1312rnmpt 5108 . . 3
146, 11, 133eqtr4i 2465 . 2
15 restval 13646 . . . . 5 t
16153adant3 977 . . . 4 t
1716oveq1d 6088 . . 3 t t t
18 ovex 6098 . . . . 5 t
1916, 18syl6eqelr 2524 . . . 4
20 simp3 959 . . . 4
21 restval 13646 . . . 4 t
2219, 20, 21syl2anc 643 . . 3 t
2317, 22eqtrd 2467 . 2 t t
24 simp1 957 . . 3
25 inex1g 4338 . . . 4