Theorem idsubfun 15206

Description: The identity restricted to the morphism of a subcategory U is a functor from the subcategory to the supercategory. It is called the inclusion functor. JFM CAT₂ th. 19.

Hypothesis

Ref	Expression
idsubfun.1	|- M = dom (dom` U)

Assertion

Ref	Expression
idsubfun	|- (U e. ( SubCat ` T) -> ( _I |` M) e. ( Func ` <.U, T>.))

Proof of Theorem idsubfun

Step	Hyp	Ref	Expression
1		besubbeca 15196	. 2 |- (U e. ( SubCat ` T) -> T e. Cat )
2		subctct 15202	. 2 |- (U e. ( SubCat ` T) -> U e. Cat )
3		fvex 4689	. . . . . . 7 |- (dom` U) e. _V
4	3	a1i 8	. . . . . 6 |- (U e. ( SubCat ` T) -> (dom` U) e. _V)
5		dmexg 4206	. . . . . 6 |- ((dom` U) e. _V -> dom (dom` U) e. _V)
6	4, 5	syl 12	. . . . 5 |- (U e. ( SubCat ` T) -> dom (dom` U) e. _V)
7		idsubfun.1	. . . . 5 |- M = dom (dom` U)
8	6, 7	syl5eqel 1975	. . . 4 |- (U e. ( SubCat ` T) -> M e. _V)
9		resiexg 4253	. . . 4 |- (M e. _V -> ( _I |` M) e. _V)
10	8, 9	syl 12	. . 3 |- (U e. ( SubCat ` T) -> ( _I |` M) e. _V)
11		eqid 1884	. . . . . . . . . . . 12 |- dom (dom` T) = dom (dom` T)
12	11, 7	morsubc 15203	. . . . . . . . . . 11 |- (U e. ( SubCat ` T) -> M C_ dom (dom` T))
13	12	adantl 424	. . . . . . . . . 10 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> M C_ dom (dom` T))
14		f1oi 4671	. . . . . . . . . . 11 |- ( _I |` M):M-1-1-onto->M
15		f1of 4635	. . . . . . . . . . 11 |- (( _I |` M):M-1-1-onto->M -> ( _I |` M):M-->M)
16	14, 15	ax-mp 7	. . . . . . . . . 10 |- ( _I |` M):M-->M
17	13, 16	jctil 316	. . . . . . . . 9 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (( _I |` M):M-->M /\ M C_ dom (dom` T)))
18		fss 4571	. . . . . . . . 9 |- ((( _I |` M):M-->M /\ M C_ dom (dom` T)) -> ( _I |` M):M-->dom (dom` T))
19	17, 18	syl 12	. . . . . . . 8 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> ( _I |` M):M-->dom (dom` T))
20		eqid 1884	. . . . . . . . . . . . 13 |- dom (id` T) = dom (id` T)
21		eqid 1884	. . . . . . . . . . . . 13 |- dom (id` U) = dom (id` U)
22	20, 21	obsubc2 15198	. . . . . . . . . . . 12 |- (U e. ( SubCat ` T) -> dom (id` U) C_ dom (id` T))
23		ssel 2615	. . . . . . . . . . . . . . . 16 |- (dom (id` U) C_ dom (id` T) -> (o e. dom (id` U) -> o e. dom (id` T)))
24		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (p = o -> ((id` T)` p) = ((id` T)` o))
25	24	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (p = o -> ((( _I |` M)` ((id` U)` o)) = ((id` T)` p) <-> (( _I |` M)` ((id` U)` o)) = ((id` T)` o)))
26	25	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- ((o e. dom (id` T) /\ (( _I |` M)` ((id` U)` o)) = ((id` T)` o)) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p))
27	26	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (o e. dom (id` T) -> ((( _I |` M)` ((id` U)` o)) = ((id` T)` o) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))
28		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- ((id` U)` o) e. _V
29		fvi 4818	. . . . . . . . . . . . . . . . . . . . 21 |- (((id` U)` o) e. _V -> ( _I ` ((id` U)` o)) = ((id` U)` o))
30	28, 29	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- ( _I ` ((id` U)` o)) = ((id` U)` o)
31		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (id` U) = (id` U)
32	7, 21, 31	jdmo 15125	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((U e. Cat /\ o e. dom (id` U)) -> ((id` U)` o) e. M)
33	32	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (U e. Cat -> (o e. dom (id` U) -> ((id` U)` o) e. M))
34	33	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . 23 |- (U e. Cat -> (o e. dom (id` U) -> (U e. ( SubCat ` T) -> ((id` U)` o) e. M)))
35	34	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . 22 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (o e. dom (id` U) -> (U e. ( SubCat ` T) -> ((id` U)` o) e. M)))
36	35	3imp 1061	. . . . . . . . . . . . . . . . . . . . 21 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> ((id` U)` o) e. M)
37		fvres 4691	. . . . . . . . . . . . . . . . . . . . 21 |- (((id` U)` o) e. M -> (( _I |` M)` ((id` U)` o)) = ( _I ` ((id` U)` o)))
38	36, 37	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> (( _I |` M)` ((id` U)` o)) = ( _I ` ((id` U)` o)))
39		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom` T) = (dom` T)
40		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (id` T) = (id` T)
41	11, 39, 20, 40	idc 15114	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (T e. Cat -> (id` T):dom (id` T)-->dom (dom` T))
42		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((id` T):dom (id` T)-->dom (dom` T) -> Fun (id` T))
43	41, 42	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- (T e. Cat -> Fun (id` T))
44	43	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . 22 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> Fun (id` T))
45	44	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . 21 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> Fun (id` T))
46	40, 31	idsubc 15199	. . . . . . . . . . . . . . . . . . . . . 22 |- (U e. ( SubCat ` T) -> (id` U) C_ (id` T))
47	46	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . 21 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> (id` U) C_ (id` T))
48		simp2 877	. . . . . . . . . . . . . . . . . . . . 21 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> o e. dom (id` U))
49		funssfv 4692	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun (id` T) /\ (id` U) C_ (id` T) /\ o e. dom (id` U)) -> ((id` T)` o) = ((id` U)` o))
50	45, 47, 48, 49	syl111anc 1100	. . . . . . . . . . . . . . . . . . . 20 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> ((id` T)` o) = ((id` U)` o))
51	30, 38, 50	3eqtr4a 1954	. . . . . . . . . . . . . . . . . . 19 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> (( _I |` M)` ((id` U)` o)) = ((id` T)` o))
52	27, 51	syl5com 63	. . . . . . . . . . . . . . . . . 18 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ o e. dom (id` U) /\ U e. ( SubCat ` T)) -> (o e. dom (id` T) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))
53	52	3exp 1066	. . . . . . . . . . . . . . . . 17 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (o e. dom (id` U) -> (U e. ( SubCat ` T) -> (o e. dom (id` T) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))))
54	53	com14 42	. . . . . . . . . . . . . . . 16 |- (o e. dom (id` T) -> (o e. dom (id` U) -> (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))))
55	23, 54	syl6 25	. . . . . . . . . . . . . . 15 |- (dom (id` U) C_ dom (id` T) -> (o e. dom (id` U) -> (o e. dom (id` U) -> (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p))))))
56	55	com13 37	. . . . . . . . . . . . . 14 |- (o e. dom (id` U) -> (o e. dom (id` U) -> (dom (id` U) C_ dom (id` T) -> (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p))))))
57	56	pm2.43i 78	. . . . . . . . . . . . 13 |- (o e. dom (id` U) -> (dom (id` U) C_ dom (id` T) -> (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))))
58	57	com4l 43	. . . . . . . . . . . 12 |- (dom (id` U) C_ dom (id` T) -> (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (o e. dom (id` U) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))))
59	22, 58	mpcom 60	. . . . . . . . . . 11 |- (U e. ( SubCat ` T) -> ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (o e. dom (id` U) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p))))
60	59	impcom 378	. . . . . . . . . 10 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (o e. dom (id` U) -> E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p)))
61	60	r19.21aiv 2175	. . . . . . . . 9 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> A.o e. dom (id` U)E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p))
62		simpll1 915	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> U e. Cat )
63		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- dom (dom` U) = dom (dom` U)
64		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (dom` U) = (dom` U)
65	63, 21, 64	dmo 15123	. . . . . . . . . . . . . . . . 17 |- ((U e. Cat /\ m e. dom (dom` U)) -> ((dom` U)` m) e. dom (id` U))
66		simpl1 879	. . . . . . . . . . . . . . . . 17 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> U e. Cat )
67	7	eleq2i 1961	. . . . . . . . . . . . . . . . . 18 |- (m e. M <-> m e. dom (dom` U))
68	67	biimpi 168	. . . . . . . . . . . . . . . . 17 |- (m e. M -> m e. dom (dom` U))
69	65, 66, 68	syl2an 503	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((dom` U)` m) e. dom (id` U))
70	7, 21, 31	jdmo 15125	. . . . . . . . . . . . . . . 16 |- ((U e. Cat /\ ((dom` U)` m) e. dom (id` U)) -> ((id` U)` ((dom` U)` m)) e. M)
71	62, 69, 70	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((dom` U)` m)) e. M)
72		fvres 4691	. . . . . . . . . . . . . . 15 |- (((id` U)` ((dom` U)` m)) e. M -> (( _I |` M)` ((id` U)` ((dom` U)` m))) = ( _I ` ((id` U)` ((dom` U)` m))))
73	71, 72	syl 12	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((dom` U)` m))) = ( _I ` ((id` U)` ((dom` U)` m))))
74		fvex 4689	. . . . . . . . . . . . . . . 16 |- ((id` U)` ((dom` U)` m)) e. _V
75	74	a1i 8	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((dom` U)` m)) e. _V)
76		fvi 4818	. . . . . . . . . . . . . . 15 |- (((id` U)` ((dom` U)` m)) e. _V -> ( _I ` ((id` U)` ((dom` U)` m))) = ((id` U)` ((dom` U)` m)))
77	75, 76	syl 12	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ( _I ` ((id` U)` ((dom` U)` m))) = ((id` U)` ((dom` U)` m)))
78	73, 77	eqtrd 1925	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` U)` ((dom` U)` m)))
79	44	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> Fun (id` T))
80	46	ad2antlr 441	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (id` U) C_ (id` T))
81		funssfv 4692	. . . . . . . . . . . . . . 15 |- ((Fun (id` T) /\ (id` U) C_ (id` T) /\ ((dom` U)` m) e. dom (id` U)) -> ((id` T)` ((dom` U)` m)) = ((id` U)` ((dom` U)` m)))
82	79, 80, 69, 81	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` T)` ((dom` U)` m)) = ((id` U)` ((dom` U)` m)))
83	11, 39, 20, 40	domc 15112	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Cat -> (dom` T):dom (dom` T)-->dom (id` T))
84		ffun 4565	. . . . . . . . . . . . . . . . . . . 20 |- ((dom` T):dom (dom` T)-->dom (id` T) -> Fun (dom` T))
85	83, 84	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (T e. Cat -> Fun (dom` T))
86	85	3ad2ant2 898	. . . . . . . . . . . . . . . . . 18 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> Fun (dom` T))
87	86	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> Fun (dom` T))
88	39, 64	domsubc 15200	. . . . . . . . . . . . . . . . . 18 |- (U e. ( SubCat ` T) -> (dom` U) C_ (dom` T))
89	88	ad2antlr 441	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (dom` U) C_ (dom` T))
90	68	adantl 424	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> m e. dom (dom` U))
91		funssfv 4692	. . . . . . . . . . . . . . . . 17 |- ((Fun (dom` T) /\ (dom` U) C_ (dom` T) /\ m e. dom (dom` U)) -> ((dom` T)` m) = ((dom` U)` m))
92	87, 89, 90, 91	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((dom` T)` m) = ((dom` U)` m))
93	92	eqcomd 1889	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((dom` U)` m) = ((dom` T)` m))
94	93	fveq2d 4685	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` T)` ((dom` U)` m)) = ((id` T)` ((dom` T)` m)))
95	82, 94	eqtr3d 1927	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((dom` U)` m)) = ((id` T)` ((dom` T)` m)))
96		fvres 4691	. . . . . . . . . . . . . . . . 17 |- (m e. M -> (( _I |` M)` m) = ( _I ` m))
97	96	adantl 424	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` m) = ( _I ` m))
98		fvi 4818	. . . . . . . . . . . . . . . . 17 |- (m e. M -> ( _I ` m) = m)
99	98	adantl 424	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ( _I ` m) = m)
100	97, 99	eqtr2d 1926	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> m = (( _I |` M)` m))
101	100	fveq2d 4685	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((dom` T)` m) = ((dom` T)` (( _I |` M)` m)))
102	101	fveq2d 4685	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` T)` ((dom` T)` m)) = ((id` T)` ((dom` T)` (( _I |` M)` m))))
103	78, 95, 102	3eqtrd 1929	. . . . . . . . . . . 12 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))))
104	103	ex 402	. . . . . . . . . . 11 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (m e. M -> (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m)))))
105	104	r19.21aiv 2175	. . . . . . . . . 10 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))))
106		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- (cod` U) = (cod` U)
107	7, 21, 106	cdmo 15124	. . . . . . . . . . . . . . . . 17 |- ((U e. Cat /\ m e. M) -> ((cod` U)` m) e. dom (id` U))
108	107, 66	sylan 497	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((cod` U)` m) e. dom (id` U))
109	7, 21, 31	jdmo 15125	. . . . . . . . . . . . . . . 16 |- ((U e. Cat /\ ((cod` U)` m) e. dom (id` U)) -> ((id` U)` ((cod` U)` m)) e. M)
110	62, 108, 109	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((cod` U)` m)) e. M)
111		fvres 4691	. . . . . . . . . . . . . . 15 |- (((id` U)` ((cod` U)` m)) e. M -> (( _I |` M)` ((id` U)` ((cod` U)` m))) = ( _I ` ((id` U)` ((cod` U)` m))))
112	110, 111	syl 12	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((cod` U)` m))) = ( _I ` ((id` U)` ((cod` U)` m))))
113		fvex 4689	. . . . . . . . . . . . . . . 16 |- ((id` U)` ((cod` U)` m)) e. _V
114	113	a1i 8	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((cod` U)` m)) e. _V)
115		fvi 4818	. . . . . . . . . . . . . . 15 |- (((id` U)` ((cod` U)` m)) e. _V -> ( _I ` ((id` U)` ((cod` U)` m))) = ((id` U)` ((cod` U)` m)))
116	114, 115	syl 12	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ( _I ` ((id` U)` ((cod` U)` m))) = ((id` U)` ((cod` U)` m)))
117	112, 116	eqtrd 1925	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` U)` ((cod` U)` m)))
118		funssfv 4692	. . . . . . . . . . . . . . . 16 |- ((Fun (id` T) /\ (id` U) C_ (id` T) /\ ((cod` U)` m) e. dom (id` U)) -> ((id` T)` ((cod` U)` m)) = ((id` U)` ((cod` U)` m)))
119	118	eqcomd 1889	. . . . . . . . . . . . . . 15 |- ((Fun (id` T) /\ (id` U) C_ (id` T) /\ ((cod` U)` m) e. dom (id` U)) -> ((id` U)` ((cod` U)` m)) = ((id` T)` ((cod` U)` m)))
120	79, 80, 108, 119	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((cod` U)` m)) = ((id` T)` ((cod` U)` m)))
121		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- (cod` T) = (cod` T)
122	11, 39, 20, 40, 121	codc 15113	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Cat -> (cod` T):dom (dom` T)-->dom (id` T))
123		ffun 4565	. . . . . . . . . . . . . . . . . . . 20 |- ((cod` T):dom (dom` T)-->dom (id` T) -> Fun (cod` T))
124	122, 123	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (T e. Cat -> Fun (cod` T))
125	124	3ad2ant2 898	. . . . . . . . . . . . . . . . . 18 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> Fun (cod` T))
126	125	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> Fun (cod` T))
127	121, 106	codsubc 15201	. . . . . . . . . . . . . . . . . 18 |- (U e. ( SubCat ` T) -> (cod` U) C_ (cod` T))
128	127	ad2antlr 441	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (cod` U) C_ (cod` T))
129		morcat 15127	. . . . . . . . . . . . . . . . . . . . . 22 |- (U e. Cat -> dom (dom` U) = dom (cod` U))
130	129, 7	syl5eq 1940	. . . . . . . . . . . . . . . . . . . . 21 |- (U e. Cat -> M = dom (cod` U))
131	130	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . 20 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> M = dom (cod` U))
132	131	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> M = dom (cod` U))
133	132	eleq2d 1964	. . . . . . . . . . . . . . . . . 18 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (m e. M <-> m e. dom (cod` U)))
134	133	biimpa 460	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> m e. dom (cod` U))
135		funssfv 4692	. . . . . . . . . . . . . . . . 17 |- ((Fun (cod` T) /\ (cod` U) C_ (cod` T) /\ m e. dom (cod` U)) -> ((cod` T)` m) = ((cod` U)` m))
136	126, 128, 134, 135	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((cod` T)` m) = ((cod` U)` m))
137	136	eqcomd 1889	. . . . . . . . . . . . . . 15 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((cod` U)` m) = ((cod` T)` m))
138	137	fveq2d 4685	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` T)` ((cod` U)` m)) = ((id` T)` ((cod` T)` m)))
139	120, 138	eqtrd 1925	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` U)` ((cod` U)` m)) = ((id` T)` ((cod` T)` m)))
140	100	fveq2d 4685	. . . . . . . . . . . . . 14 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((cod` T)` m) = ((cod` T)` (( _I |` M)` m)))
141	140	fveq2d 4685	. . . . . . . . . . . . 13 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> ((id` T)` ((cod` T)` m)) = ((id` T)` ((cod` T)` (( _I |` M)` m))))
142	117, 139, 141	3eqtrd 1929	. . . . . . . . . . . 12 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m))))
143	142	ex 402	. . . . . . . . . . 11 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (m e. M -> (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))))
144	143	r19.21aiv 2175	. . . . . . . . . 10 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m))))
145	105, 144	jca 310	. . . . . . . . 9 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))) /\ A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))))
146		id 73	. . . . . . . . . . . . . . . . . . . . . 22 |- ((U e. Cat /\ n e. M /\ m e. M) -> (U e. Cat /\ n e. M /\ m e. M))
147	146	3exp 1066	. . . . . . . . . . . . . . . . . . . . 21 |- (U e. Cat -> (n e. M -> (m e. M -> (U e. Cat /\ n e. M /\ m e. M))))
148	147	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- (U e. Cat -> (m e. M -> (n e. M -> (U e. Cat /\ n e. M /\ m e. M))))
149	148	3ad2ant1 897	. . . . . . . . . . . . . . . . . . 19 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (m e. M -> (n e. M -> (U e. Cat /\ n e. M /\ m e. M))))
150	149	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (m e. M -> (n e. M -> (U e. Cat /\ n e. M /\ m e. M))))
151	150	imp31 389	. . . . . . . . . . . . . . . . 17 |- (((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) -> (U e. Cat /\ n e. M /\ m e. M))
152	151	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (U e. Cat /\ n e. M /\ m e. M))
153		id 73	. . . . . . . . . . . . . . . . . 18 |- (((cod` U)` n) = ((dom` U)` m) -> ((cod` U)` n) = ((dom` U)` m))
154	153	eqcomd 1889	. . . . . . . . . . . . . . . . 17 |- (((cod` U)` n) = ((dom` U)` m) -> ((dom` U)` m) = ((cod` U)` n))
155	154	adantl 424	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> ((dom` U)` m) = ((cod` U)` n))
156		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (o` U) = (o` U)
157	7, 64, 106, 156	cmpmorp 15126	. . . . . . . . . . . . . . . 16 |- ((U e. Cat /\ n e. M /\ m e. M) -> (((dom` U)` m) = ((cod` U)` n) -> (m(o` U)n) e. M))
158	152, 155, 157	sylc 83	. . . . . . . . . . . . . . 15 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (m(o` U)n) e. M)
159		fvres 4691	. . . . . . . . . . . . . . 15 |- ((m(o` U)n) e. M -> (( _I |` M)` (m(o` U)n)) = ( _I ` (m(o` U)n)))
160	158, 159	syl 12	. . . . . . . . . . . . . 14 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (( _I |` M)` (m(o` U)n)) = ( _I ` (m(o` U)n)))
161		oprex 4907	. . . . . . . . . . . . . . . 16 |- (m(o` U)n) e. _V
162		fvi 4818	. . . . . . . . . . . . . . . 16 |- ((m(o` U)n) e. _V -> ( _I ` (m(o` U)n)) = (m(o` U)n))
163	161, 162	ax-mp 7	. . . . . . . . . . . . . . 15 |- ( _I ` (m(o` U)n)) = (m(o` U)n)
164	163	a1i 8	. . . . . . . . . . . . . 14 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> ( _I ` (m(o` U)n)) = (m(o` U)n))
165		fvresi 4819	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. M -> (( _I |` M)` m) = m)
166	165	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. M /\ n e. M) -> (( _I |` M)` m) = m)
167	166	eqcomd 1889	. . . . . . . . . . . . . . . . . . 19 |- ((m e. M /\ n e. M) -> m = (( _I |` M)` m))
168		fvres 4691	. . . . . . . . . . . . . . . . . . . . 21 |- (n e. M -> (( _I |` M)` n) = ( _I ` n))
169	168	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. M /\ n e. M) -> (( _I |` M)` n) = ( _I ` n))
170		fvi 4818	. . . . . . . . . . . . . . . . . . . . 21 |- (n e. M -> ( _I ` n) = n)
171	170	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. M /\ n e. M) -> ( _I ` n) = n)
172	169, 171	eqtr2d 1926	. . . . . . . . . . . . . . . . . . 19 |- ((m e. M /\ n e. M) -> n = (( _I |` M)` n))
173	167, 172	jca 310	. . . . . . . . . . . . . . . . . 18 |- ((m e. M /\ n e. M) -> (m = (( _I |` M)` m) /\ n = (( _I |` M)` n)))
174	173	adantll 428	. . . . . . . . . . . . . . . . 17 |- (((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) -> (m = (( _I |` M)` m) /\ n = (( _I |` M)` n)))
175	174	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (m = (( _I |` M)` m) /\ n = (( _I |` M)` n)))
176		opreq12 4891	. . . . . . . . . . . . . . . 16 |- ((m = (( _I |` M)` m) /\ n = (( _I |` M)` n)) -> (m(o` U)n) = ((( _I |` M)` m)(o` U)(( _I |` M)` n)))
177	175, 176	syl 12	. . . . . . . . . . . . . . 15 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (m(o` U)n) = ((( _I |` M)` m)(o` U)(( _I |` M)` n)))
178		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- (o` T) = (o` T)
179	178	cmppfc1 15128	. . . . . . . . . . . . . . . . . . 19 |- (T e. Cat -> Fun (o` T))
180	179	3ad2ant2 898	. . . . . . . . . . . . . . . . . 18 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> Fun (o` T))
181	180	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> Fun (o` T))
182	181	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> Fun (o` T))
183	178, 156	cmpsubc 15204	. . . . . . . . . . . . . . . . . 18 |- (U e. ( SubCat ` T) -> (o` U) C_ (o` T))
184	183	ad2antlr 441	. . . . . . . . . . . . . . . . 17 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (o` U) C_ (o` T))
185	184	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (o` U) C_ (o` T))
186	165	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (( _I |` M)` m) = m)
187	186	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (( _I |` M)` m) = m)
188		fvresi 4819	. . . . . . . . . . . . . . . . . . 19 |- (n e. M -> (( _I |` M)` n) = n)
189	188	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (( _I |` M)` n) = n)
190	187, 189	opeq12d 3166	. . . . . . . . . . . . . . . . 17 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> <.(( _I |` M)` m), (( _I |` M)` n)>. = <.m, n>.)
191	7, 64, 106, 156	cmppfcd 15117	. . . . . . . . . . . . . . . . . . 19 |- ((U e. Cat /\ n e. M /\ m e. M) -> (<.m, n>. e. dom (o` U) <-> ((dom` U)` m) = ((cod` U)` n)))
192	152, 191	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (<.m, n>. e. dom (o` U) <-> ((dom` U)` m) = ((cod` U)` n)))
193	155, 192	mpbird 213	. . . . . . . . . . . . . . . . 17 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> <.m, n>. e. dom (o` U))
194	190, 193	eqeltrd 1971	. . . . . . . . . . . . . . . 16 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> <.(( _I |` M)` m), (( _I |` M)` n)>. e. dom (o` U))
195		oprssoprvg 14335	. . . . . . . . . . . . . . . 16 |- ((Fun (o` T) /\ (o` U) C_ (o` T) /\ <.(( _I |` M)` m), (( _I |` M)` n)>. e. dom (o` U)) -> ((( _I |` M)` m)(o` T)(( _I |` M)` n)) = ((( _I |` M)` m)(o` U)(( _I |` M)` n)))
196	182, 185, 194, 195	syl111anc 1100	. . . . . . . . . . . . . . 15 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> ((( _I |` M)` m)(o` T)(( _I |` M)` n)) = ((( _I |` M)` m)(o` U)(( _I |` M)` n)))
197	177, 196	eqtr4d 1928	. . . . . . . . . . . . . 14 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (m(o` U)n) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))
198	160, 164, 197	3eqtrd 1929	. . . . . . . . . . . . 13 |- ((((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) /\ n e. M) /\ ((cod` U)` n) = ((dom` U)` m)) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))
199	198	exp31 407	. . . . . . . . . . . 12 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> (n e. M -> (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))))
200	199	r19.21aiv 2175	. . . . . . . . . . 11 |- ((((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) /\ m e. M) -> A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n))))
201	200	ex 402	. . . . . . . . . 10 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (m e. M -> A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))))
202	201	r19.21aiv 2175	. . . . . . . . 9 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> A.m e. M A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n))))
203	61, 145, 202	3jca 1050	. . . . . . . 8 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (A.o e. dom (id` U)E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p) /\ (A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))) /\ A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))) /\ A.m e. M A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))))
204	19, 203	jca 310	. . . . . . 7 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (( _I |` M):M-->dom (dom` T) /\ (A.o e. dom (id` U)E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p) /\ (A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))) /\ A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))) /\ A.m e. M A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n))))))
205	21, 7, 64, 106, 31, 156, 20, 11, 39, 121, 40, 178	isfunb 15183	. . . . . . . 8 |- ((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) -> (( _I |` M) e. ( Func ` <.U, T>.) <-> (( _I |` M):M-->dom (dom` T) /\ (A.o e. dom (id` U)E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p) /\ (A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))) /\ A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))) /\ A.m e. M A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))))))
206	205	adantr 425	. . . . . . 7 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> (( _I |` M) e. ( Func ` <.U, T>.) <-> (( _I |` M):M-->dom (dom` T) /\ (A.o e. dom (id` U)E.p e. dom (id` T)(( _I |` M)` ((id` U)` o)) = ((id` T)` p) /\ (A.m e. M (( _I |` M)` ((id` U)` ((dom` U)` m))) = ((id` T)` ((dom` T)` (( _I |` M)` m))) /\ A.m e. M (( _I |` M)` ((id` U)` ((cod` U)` m))) = ((id` T)` ((cod` T)` (( _I |` M)` m)))) /\ A.m e. M A.n e. M (((cod` U)` n) = ((dom` U)` m) -> (( _I |` M)` (m(o` U)n)) = ((( _I |` M)` m)(o` T)(( _I |` M)` n)))))))
207	204, 206	mpbird 213	. . . . . 6 |- (((U e. Cat /\ T e. Cat /\ ( _I |` M) e. _V) /\ U e. ( SubCat ` T)) -> ( _I |` M) e. ( Func ` <.U, T>.))
208	207	3exp1 1084	. . . . 5 |- (U e. Cat -> (T e. Cat -> (( _I |` M) e. _V -> (U e. ( SubCat ` T) -> ( _I |` M) e. ( Func ` <.U, T>.)))))
209	208	impcom 378	. . . 4 |- ((T e. Cat /\ U e. Cat ) -> (( _I |` M) e. _V -> (U e. ( SubCat ` T) -> ( _I |` M) e. ( Func ` <.U, T>.))))
210	209	com13 37	. . 3 |- (U e. ( SubCat ` T) -> (( _I |` M) e. _V -> ((T e. Cat /\ U e. Cat ) -> ( _I |` M) e. ( Func ` <.U, T>.))))
211	10, 210	mpd 29	. 2 |- (U e. ( SubCat ` T) -> ((T e. Cat /\ U e. Cat ) -> ( _I |` M) e. ( Func ` <.U, T>.)))
212	1, 2, 211	mp2and 767	1 |- (U e. ( SubCat ` T) -> ( _I |` M) e. ( Func ` <.U, T>.))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  <.cop 3046   _I cid 3582  dom cdm 3986   |` cres 3988  Fun wfun 3992  -->wf 3994  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062   Cat ccat 15099   Func cfunc 15179   SubCat csubc 15191

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-map 5383  df-alg 15063  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-ded 15082  df-cat 15100  df-func 15181  df-subc 15192

Copyright terms: Public domain