Theorem isfuna 10664

Description: The class of functors between T and U.

Hypotheses

Ref	Expression
isfuna.1	|- O1 = dom (id` T)
isfuna.2	|- M1 = dom (dom` T)
isfuna.3	|- D1 = (dom` T)
isfuna.4	|- C1 = (cod` T)
isfuna.5	|- I1 = (id` T)
isfuna.6	|- Ro1 = (o` T)
isfuna.7	|- O2 = dom (id` U)
isfuna.8	|- M2 = dom (dom` U)
isfuna.9	|- D2 = (dom` U)
isfuna.10	|- C2 = (cod` U)
isfuna.11	|- I2 = (id` U)
isfuna.12	|- Ro2 = (o` U)

Assertion

Ref	Expression
isfuna	|- ((T e. Cat /\ U e. Cat) -> (Func` <.T, U>.) = {f | (f:M1-->M2 /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))})

Distinct variable groups:   f,M₁,m   f,M₂   o,O₁   p,O₂   T,f,m,n,o,p   U,f,m,n,o,p

Proof of Theorem isfuna

Step	Hyp	Ref	Expression
1		isfuna.8	. . . . . . . . 9 |- M2 = dom (dom` U)
2		fvex 3727	. . . . . . . . . 10 |- (dom` U) e. V
3	2	dmex 3356	. . . . . . . . 9 |- dom (dom` U) e. V
4	1, 3	eqeltr 1542	. . . . . . . 8 |- M2 e. V
5		isfuna.2	. . . . . . . . 9 |- M1 = dom (dom` T)
6		fvex 3727	. . . . . . . . . 10 |- (dom` T) e. V
7	6	dmex 3356	. . . . . . . . 9 |- dom (dom` T) e. V
8	5, 7	eqeltr 1542	. . . . . . . 8 |- M1 e. V
9	4, 8	pm3.2i 285	. . . . . . 7 |- (M2 e. V /\ M1 e. V)
10	9	a1i 8	. . . . . 6 |- ((T e. Cat /\ U e. Cat) -> (M2 e. V /\ M1 e. V))
11		elmapg 4326	. . . . . 6 |- ((M2 e. V /\ M1 e. V) -> (f e. (M2 ^m M1) <-> f:M1-->M2))
12	10, 11	syl 10	. . . . 5 |- ((T e. Cat /\ U e. Cat) -> (f e. (M2 ^m M1) <-> f:M1-->M2))
13	12	anbi1d 616	. . . 4 |- ((T e. Cat /\ U e. Cat) -> ((f e. (M2 ^m M1) /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))))) <-> (f:M1-->M2 /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))))
14	13	abbidv 1575	. . 3 |- ((T e. Cat /\ U e. Cat) -> {f | (f e. (M2 ^m M1) /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))} = {f | (f:M1-->M2 /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))})
15	9	a1i 8	. . . . . . . 8 |- ((U e. Cat /\ T e. Cat) -> (M2 e. V /\ M1 e. V))
16		mapvalg 4323	. . . . . . . 8 |- ((M2 e. V /\ M1 e. V) -> (M2 ^m M1) = {x | x:M1-->M2})
17	15, 16	syl 10	. . . . . . 7 |- ((U e. Cat /\ T e. Cat) -> (M2 ^m M1) = {x | x:M1-->M2})
18	17	ancoms 436	. . . . . 6 |- ((T e. Cat /\ U e. Cat) -> (M2 ^m M1) = {x | x:M1-->M2})
19	8, 4	pm3.2i 285	. . . . . . . 8 |- (M1 e. V /\ M2 e. V)
20	19	a1i 8	. . . . . . 7 |- ((T e. Cat /\ U e. Cat) -> (M1 e. V /\ M2 e. V))
21		mapex 4321	. . . . . . 7 |- ((M1 e. V /\ M2 e. V) -> {x | x:M1-->M2} e. V)
22	20, 21	syl 10	. . . . . 6 |- ((T e. Cat /\ U e. Cat) -> {x | x:M1-->M2} e. V)
23	18, 22	eqeltrd 1546	. . . . 5 |- ((T e. Cat /\ U e. Cat) -> (M2 ^m M1) e. V)
24		rabexg 2720	. . . . 5 |- ((M2 ^m M1) e. V -> {f e. (M2 ^m M1) | (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))))} e. V)
25	23, 24	syl 10	. . . 4 |- ((T e. Cat /\ U e. Cat) -> {f e. (M2 ^m M1) | (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))))} e. V)
26		df-rab 1650	. . . 4 |- {f e. (M2 ^m M1) | (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))))} = {f | (f e. (M2 ^m M1) /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))}
27	25, 26	syl5eqelr 1551	. . 3 |- ((T e. Cat /\ U e. Cat) -> {f | (f e. (M2 ^m M1) /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))} e. V)
28	14, 27	eqeltrrd 1547	. 2 |- ((T e. Cat /\ U e. Cat) -> {f | (f:M1-->M2 /\ (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) /\ (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) /\ A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m)))) /\ A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n)))))} e.