Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  idsubfun Unicode version

Theorem idsubfun 25961
 Description: The identity restricted to the morphism of a subcategory is a functor from the subcategory to the supercategory. It is called the inclusion functor. JFM CAT2 th. 19. (Contributed by FL, 5-Oct-2009.)
Hypothesis
Ref Expression
idsubfun.1
Assertion
Ref Expression
idsubfun

Proof of Theorem idsubfun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oi 5527 . . . 4
2 f1of 5488 . . . 4
31, 2ax-mp 8 . . 3
4 eqid 2296 . . . 4
5 idsubfun.1 . . . 4
64, 5morsubc 25958 . . 3
7 fss 5413 . . 3
83, 6, 7sylancr 644 . 2
9 eqid 2296 . . . . . . 7
10 eqid 2296 . . . . . . 7
119, 10obsubc2 25953 . . . . . 6
1211sselda 3193 . . . . 5
13 fvex 5555 . . . . . . 7
14 fvi 5595 . . . . . . 7
1513, 14ax-mp 8 . . . . . 6
16 subctct 25957 . . . . . . . 8
17 eqid 2296 . . . . . . . . 9
185, 10, 17jdmo 25881 . . . . . . . 8
1916, 18sylan 457 . . . . . . 7
20 fvres 5558 . . . . . . 7
2119, 20syl 15 . . . . . 6
22 besubbeca 25951 . . . . . . . . 9
23 eqid 2296 . . . . . . . . . 10
24 eqid 2296 . . . . . . . . . 10
254, 23, 9, 24idc 25870 . . . . . . . . 9
26 ffun 5407 . . . . . . . . 9
2722, 25, 263syl 18 . . . . . . . 8
2827adantr 451 . . . . . . 7
2924, 17idsubc 25954 . . . . . . . 8
3029adantr 451 . . . . . . 7
31 simpr 447 . . . . . . 7
32 funssfv 5559 . . . . . . 7
3328, 30, 31, 32syl3anc 1182 . . . . . 6
3415, 21, 333eqtr4a 2354 . . . . 5
35 fveq2 5541 . . . . . . 7
3635eqeq2d 2307 . . . . . 6
3736rspcev 2897 . . . . 5
3812, 34, 37syl2anc 642 . . . 4
3938ralrimiva 2639 . . 3
4016adantr 451 . . . . . . . 8
415eleq2i 2360 . . . . . . . . . 10
4241biimpi 186 . . . . . . . . 9
43 eqid 2296 . . . . . . . . . 10
44 eqid 2296 . . . . . . . . . 10
4543, 10, 44dmo 25879 . . . . . . . . 9
4616, 42, 45syl2an 463 . . . . . . . 8
475, 10, 17jdmo 25881 . . . . . . . 8
4840, 46, 47syl2anc 642 . . . . . . 7
49 fvres 5558 . . . . . . 7
5048, 49syl 15 . . . . . 6
51 fvex 5555 . . . . . . 7
52 fvi 5595 . . . . . . 7
5351, 52mp1i 11 . . . . . 6
544, 23, 9, 24domc 25868 . . . . . . . . . . . 12
55 ffun 5407 . . . . . . . . . . . 12
5622, 54, 553syl 18 . . . . . . . . . . 11
5756adantr 451 . . . . . . . . . 10
5823, 44domsubc 25955 . . . . . . . . . . 11
5958adantr 451 . . . . . . . . . 10
6042adantl 452 . . . . . . . . . 10
61 funssfv 5559 . . . . . . . . . 10
6257, 59, 60, 61syl3anc 1182 . . . . . . . . 9
6362eqcomd 2301 . . . . . . . 8
6463fveq2d 5545 . . . . . . 7
6527adantr 451 . . . . . . . 8
6629adantr 451 . . . . . . . 8
67 funssfv 5559 . . . . . . . 8
6865, 66, 46, 67syl3anc 1182 . . . . . . 7
69 fvres 5558 . . . . . . . . . . 11
7069adantl 452 . . . . . . . . . 10
71 fvi 5595 . . . . . . . . . . 11
7271adantl 452 . . . . . . . . . 10
7370, 72eqtr2d 2329 . . . . . . . . 9
7473fveq2d 5545 . . . . . . . 8
7574fveq2d 5545 . . . . . . 7
7664, 68, 753eqtr3d 2336 . . . . . 6
7750, 53, 763eqtrd 2332 . . . . 5
7877ralrimiva 2639 . . . 4
79 eqid 2296 . . . . . . . . . 10
805, 10, 79cdmo 25880 . . . . . . . . 9
8116, 80sylan 457 . . . . . . . 8
825, 10, 17jdmo 25881 . . . . . . . 8
8340, 81, 82syl2anc 642 . . . . . . 7
84 fvres 5558 . . . . . . 7
8583, 84syl 15 . . . . . 6
86 fvex 5555 . . . . . . 7
87 fvi 5595 . . . . . . 7
8886, 87mp1i 11 . . . . . 6
89 funssfv 5559 . . . . . . . . 9
9089eqcomd 2301 . . . . . . . 8
9165, 66, 81, 90syl3anc 1182 . . . . . . 7
92 eqid 2296 . . . . . . . . . . . . 13
934, 23, 9, 24, 92codc 25869 . . . . . . . . . . . 12
94 ffun 5407 . . . . . . . . . . . 12
9522, 93, 943syl 18 . . . . . . . . . . 11
9695adantr 451 . . . . . . . . . 10
9792, 79codsubc 25956 . . . . . . . . . . 11
9897adantr 451 . . . . . . . . . 10
99 morcat 25883 . . . . . . . . . . . . . 14
1005, 99syl5eq 2340 . . . . . . . . . . . . 13
10116, 100syl 15 . . . . . . . . . . . 12
102101eleq2d 2363 . . . . . . . . . . 11
103102biimpa 470 . . . . . . . . . 10
104 funssfv 5559 . . . . . . . . . 10
10596, 98, 103, 104syl3anc 1182 . . . . . . . . 9
106105eqcomd 2301 . . . . . . . 8
107106fveq2d 5545 . . . . . . 7
10873fveq2d 5545 . . . . . . . 8
109108fveq2d 5545 . . . . . . 7
11091, 107, 1093eqtrd 2332 . . . . . 6
11185, 88, 1103eqtrd 2332 . . . . 5
112111ralrimiva 2639 . . . 4
11378, 112jca 518 . . 3
114 pm3.2an3 1131 . . . . . . . . . . . . 13
115114com23 72 . . . . . . . . . . . 12
11616, 115syl 15 . . . . . . . . . . 11
117116imp31 421 . . . . . . . . . 10
118117adantr 451 . . . . . . . . 9
119 id 19 . . . . . . . . . . 11
120119eqcomd 2301 . . . . . . . . . 10
121120adantl 452 . . . . . . . . 9
122 eqid 2296 . . . . . . . . . 10
1235, 44, 79, 122cmpmorp 25882 . . . . . . . . 9
124118, 121, 123sylc 56 . . . . . . . 8
125 fvres 5558 . . . . . . . 8
126124, 125syl 15 . . . . . . 7
127 ovex 5899 . . . . . . . 8
128 fvi 5595 . . . . . . . 8
129127, 128mp1i 11 . . . . . . 7
130 fvresi 5727 . . . . . . . . . . . . . 14
131130adantr 451 . . . . . . . . . . . . 13
132131eqcomd 2301 . . . . . . . . . . . 12
133 fvres 5558 . . . . . . . . . . . . . 14
134133adantl 452 . . . . . . . . . . . . 13
135 fvi 5595 . . . . . . . . . . . . . 14
136135adantl 452 . . . . . . . . . . . . 13
137134, 136eqtr2d 2329 . . . . . . . . . . . 12
138132, 137jca 518 . . . . . . . . . . 11
139138adantll 694 . . . . . . . . . 10
140139adantr 451 . . . . . . . . 9
141 oveq12 5883 . . . . . . . . 9
142140, 141syl 15 . . . . . . . 8
143 eqid 2296 . . . . . . . . . . . . 13
144143cmppfc1 25884 . . . . . . . . . . . 12
14522, 144syl 15 . . . . . . . . . . 11
146145adantr 451 . . . . . . . . . 10
147146ad2antrr 706 . . . . . . . . 9
148143, 122cmpsubc 25959 . . . . . . . . . . 11
149148adantr 451 . . . . . . . . . 10
150149ad2antrr 706 . . . . . . . . 9
151130adantl 452 . . . . . . . . . . . 12
152151ad2antrr 706 . . . . . . . . . . 11
153 fvresi 5727 . . . . . . . . . . . 12
154153ad2antlr 707 . . . . . . . . . . 11
155152, 154opeq12d 3820 . . . . . . . . . 10
1565, 44, 79, 122cmppfcd 25873 . . . . . . . . . . . 12
157118, 156syl 15 . . . . . . . . . . 11
158121, 157mpbird 223 . . . . . . . . . 10
159155, 158eqeltrd 2370 . . . . . . . . 9
160 oprssopvg 25137 . . . . . . . . 9
161147, 150, 159, 160syl3anc 1182 . . . . . . . 8
162142, 161eqtr4d 2331 . . . . . . 7
163126, 129, 1623eqtrd 2332 . . . . . 6
164163exp31 587 . . . . 5
165164ralrimiv 2638 . . . 4
166165ralrimiva 2639 . . 3
16739, 113, 1663jca 1132 . 2
16810, 5, 44, 79, 17, 122, 9, 4, 23, 92, 24, 143isfunb 25938 . . 3
16916, 22, 168syl2anc 642 . 2
1708, 167, 169mpbir2and 888 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1632   wcel 1696  wral 2556  wrex 2557  cvv 2801   wss 3165  cop 3656   cid 4320   cdm 4705   cres 4707   wfun 5265  wf 5267  wf1o 5270  cfv 5271  (class class class)co 5874  cdom_ 25815  ccod_ 25816  cid_ 25817  co_ 25818   ccatOLD 25855  cfuncOLD 25934   csubcat 25946 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-int 3879  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-map 6790  df-alg 25819  df-dom_ 25820  df-cod_ 25821  df-id_ 25822  df-cmpa 25823  df-ded 25838  df-catOLD 25856  df-funcOLD 25936  df-subcat 25947
 Copyright terms: Public domain W3C validator