Table of ContentsTable of Contents User Sandbox < Previous   Next >
Related theorems
Unicode version
Theorem isfuna 10754
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,M1,m   f,M2   o,O1   p,O2   T,f,m,n,o,p   U,f,m,n,o,p
Proof of Theorem isfuna
StepHypRef Expression
1 isfuna.8 . . . . . . . . 9 |- M2 = dom (dom` U)
2 fvex 3732 . . . . . . . . . 10 |- (dom` U) e. V
32dmex 3360 . . . . . . . . 9 |- dom (dom` U) e. V
41, 3eqeltr 1544 . . . . . . . 8 |- M2 e. V
5 isfuna.2 . . . . . . . . 9 |- M1 = dom (dom` T)
6 fvex 3732 . . . . . . . . . 10 |- (dom` T) e. V
76dmex 3360 . . . . . . . . 9 |- dom (dom` T) e. V
85, 7eqeltr 1544 . . . . . . . 8 |- M1 e. V
94, 8pm3.2i 285 . . . . . . 7 |- (M2 e. V /\ M1 e. V)
109a1i 8 . . . . . 6 |- ((T e. Cat /\ U e. Cat) -> (M2 e. V /\ M1 e. V))
11 elmapg 4333 . . . . . 6 |- ((M2 e. V /\ M1 e. V) -> (f e. (M2 ^m M1) <-> f:M1-->M2))
1210, 11syl 10 . . . . 5 |- ((T e. Cat /\ U e. Cat) -> (f e. (M2 ^m M1) <-> f:M1-->M2))
1312anbi1d 617 . . . 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)))))))
1413abbidv 1577 . . 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)))))})
159a1i 8 . . . . . . . 8 |- ((U e. Cat /\ T e. Cat) -> (M2 e. V /\ M1 e. V))
16 mapvalg 4330 . . . . . . . 8 |- ((M2 e. V /\ M1 e. V) -> (M2 ^m M1) = {x | x:M1-->M2})
1715, 16syl 10 . . . . . . 7 |- ((U e. Cat /\ T e. Cat) -> (M2 ^m M1) = {x | x:M1-->M2})
1817ancoms 436 . . . . . 6 |- ((T e. Cat /\ U e. Cat) -> (M2 ^m M1) = {x | x:M1-->M2})
198, 4pm3.2i 285 . . . . . . . 8 |- (M1 e. V /\ M2 e. V)
2019a1i 8 . . . . . . 7 |- ((T e. Cat /\ U e. Cat) -> (M1 e. V /\ M2 e. V))
21 mapex 4328 . . . . . . 7 |- ((M1 e. V /\ M2 e. V) -> {x | x:M1-->M2} e. V)
2220, 21syl 10 . . . . . 6 |- ((T e. Cat /\ U e. Cat) -> {x | x:M1-->M2} e. V)
2318, 22eqeltrd 1548 . . . . 5 |- ((T e. Cat /\ U e. Cat) -> (M2 ^m M1) e. V)
24 rabexg 2724 . . . . 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)
2523, 24syl 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 1652 . . . 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)))))}
2725, 26syl5eqelr 1553 . . 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)
2814, 27eqeltrrd 1549 . 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)))))