Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  restco Unicode version

Theorem restco 12357
 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 2689 . . . . 5
21inex1 4062 . . . 4
3 ineq1 3270 . . . . 5
4 inass 3286 . . . . 5
53, 4syl6eq 2188 . . . 4
62, 5abrexco 5660 . . 3
7 eqid 2139 . . . . . 6
87rnmpt 4787 . . . . 5
9 mpteq1 4012 . . . . 5
108, 9ax-mp 5 . . . 4
1110rnmpt 4787 . . 3
12 eqid 2139 . . . 4
1312rnmpt 4787 . . 3
146, 11, 133eqtr4i 2170 . 2
15 restval 12140 . . . . 5 t
16153adant3 1001 . . . 4 t
1716oveq1d 5789 . . 3 t t t
18 restfn 12138 . . . . . 6 t
19 simp1 981 . . . . . . 7
2019elexd 2699 . . . . . 6
21 simp2 982 . . . . . . 7
2221elexd 2699 . . . . . 6
23 fnovex 5804 . . . . . 6 t t
2418, 20, 22, 23mp3an2i 1320 . . . . 5 t
2516, 24eqeltrrd 2217 . . . 4
26 simp3 983 . . . 4
27 restval 12140 . . . 4 t
2825, 26, 27syl2anc 408 . . 3 t
2917, 28eqtrd 2172 . 2 t t
30 inex1g 4064 . . . 4