Theorem isfunb 10755

Description: The predicate "is a functor" .

Hypotheses

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

Assertion

Ref	Expression
isfunb	|- ((T e. Cat /\ U e. Cat /\ F e. A) -> (F e. (Func` <.T, U>.) <-> (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:   m,F,n,o,p   m,M₁   o,O₁   p,O₂   T,m,n,o,p   U,m,n,o,p

Proof of Theorem isfunb

Step	Hyp	Ref	Expression
1		isfunb.1	. . . . 5 |- O1 = dom (id` T)
2		isfunb.2	. . . . 5 |- M1 = dom (dom` T)
3		isfunb.3	. . . . 5 |- D1 = (dom` T)
4		isfunb.4	. . . . 5 |- C1 = (cod` T)
5		isfunb.5	. . . . 5 |- I1 = (id` T)
6		isfunb.6	. . . . 5 |- Ro1 = (o` T)
7		isfunb.7	. . . . 5 |- O2 = dom (id` U)
8		isfunb.8	. . . . 5 |- M2 = dom (dom` U)
9		isfunb.9	. . . . 5 |- D2 = (dom` U)
10		isfunb.10	. . . . 5 |- C2 = (cod` U)
11		isfunb.11	. . . . 5 |- I2 = (id` U)
12		isfunb.12	. . . . 5 |- Ro2 = (o` U)
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	isfuna 10754	. . . 4 |- ((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)))))})
14	13	3adant3 799	. . 3 |- ((T e. Cat /\ U e. Cat /\ F e. A) -> (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)))))})
15	14	eleq2d 1541	. 2 |- ((T e. Cat /\ U e. Cat /\ F e. A) -> (F e. (Func` <.T, U>.) <-> F e. {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)))))}))
16		feq1 3620	. . . . 5 |- (f = F -> (f:M1-->M2 <-> F:M1-->M2))
17		fveq1 3723	. . . . . . . . 9 |- (f = F -> (f` (I1` o)) = (F` (I1` o)))
18	17	eqeq1d 1483	. . . . . . . 8 |- (f = F -> ((f` (I1` o)) = (I2` p) <-> (F` (I1` o)) = (I2` p)))
19	18	rexbidv 1664	. . . . . . 7 |- (f = F -> (E.p e. O2 (f` (I1` o)) = (I2` p) <-> E.p e. O2 (F` (I1` o)) = (I2` p)))
20	19	ralbidv 1663	. . . . . 6 |- (f = F -> (A.o e. O1 E.p e. O2 (f` (I1` o)) = (I2` p) <-> A.o e. O1 E.p e. O2 (F` (I1` o)) = (I2` p)))
21		fveq1 3723	. . . . . . . . 9 |- (f = F -> (f` (I1` (D1` m))) = (F` (I1` (D1` m))))
22		fveq1 3723	. . . . . . . . . . 11 |- (f = F -> (f` m) = (F` m))
23	22	fveq2d 3728	. . . . . . . . . 10 |- (f = F -> (D2` (f` m)) = (D2` (F` m)))
24	23	fveq2d 3728	. . . . . . . . 9 |- (f = F -> (I2` (D2` (f` m))) = (I2` (D2` (F` m))))
25	21, 24	eqeq12d 1489	. . . . . . . 8 |- (f = F -> ((f` (I1` (D1` m))) = (I2` (D2` (f` m))) <-> (F` (I1` (D1` m))) = (I2` (D2` (F` m)))))
26	25	ralbidv 1663	. . . . . . 7 |- (f = F -> (A.m e. M1 (f` (I1` (D1` m))) = (I2` (D2` (f` m))) <-> A.m e. M1 (F` (I1` (D1` m))) = (I2` (D2` (F` m)))))
27		fveq1 3723	. . . . . . . . 9 |- (f = F -> (f` (I1` (C1` m))) = (F` (I1` (C1` m))))
28	22	fveq2d 3728	. . . . . . . . . 10 |- (f = F -> (C2` (f` m)) = (C2` (F` m)))
29	28	fveq2d 3728	. . . . . . . . 9 |- (f = F -> (I2` (C2` (f` m))) = (I2` (C2` (F` m))))
30	27, 29	eqeq12d 1489	. . . . . . . 8 |- (f = F -> ((f` (I1` (C1` m))) = (I2` (C2` (f` m))) <-> (F` (I1` (C1` m))) = (I2` (C2` (F` m)))))
31	30	ralbidv 1663	. . . . . . 7 |- (f = F -> (A.m e. M1 (f` (I1` (C1` m))) = (I2` (C2` (f` m))) <-> A.m e. M1 (F` (I1` (C1` m))) = (I2` (C2` (F` m)))))
32	26, 31	anbi12d 628	. . . . . 6 |- (f = F -> ((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 (F` (I1` (D1` m))) = (I2` (D2` (F` m))) /\ A.m e. M1 (F` (I1` (C1` m))) = (I2` (C2` (F` m))))))
33		fveq1 3723	. . . . . . . . 9 |- (f = F -> (f` (mRo1n)) = (F` (mRo1n)))
34		fveq1 3723	. . . . . . . . . 10 |- (f = F -> (f` n) = (F` n))
35	22, 34	opreq12d 3978	. . . . . . . . 9 |- (f = F -> ((f` m)Ro2(f` n)) = ((F` m)Ro2(F` n)))
36	33, 35	eqeq12d 1489	. . . . . . . 8 |- (f = F -> ((f` (mRo1n)) = ((f` m)Ro2(f` n)) <-> (F` (mRo1n)) = ((F` m)Ro2(F` n))))
37	36	imbi2d 612	. . . . . . 7 |- (f = F -> (((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))) <-> ((C1` n) = (D1` m) -> (F` (mRo1n)) = ((F` m)Ro2(F` n)))))
38	37	2ralbidv 1680	. . . . . 6 |- (f = F -> (A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (f` (mRo1n)) = ((f` m)Ro2(f` n))) <-> A.m e. M1 A.n e. M1 ((C1` n) = (D1` m) -> (F` (mRo1n)) = ((F` m)Ro2(F` n)))))
39	20, 32, 38	3anbi123d 893	. . . . 5 |- (f = F -> ((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)) = ((