Theorem catded 15111

Description: A category is a deductive system.

Assertion

Ref	Expression
catded	|- (T e. Cat -> T e. Ded )

Proof of Theorem catded

Step	Hyp	Ref	Expression
1		relcat 15108	. . . . 5 |- Rel Cat
2		reldcat 15109	. . . . 5 |- Rel dom Cat
3		relrcat 15110	. . . . 5 |- Rel ran Cat
4	1, 2, 3	3pm3.2i 1048	. . . 4 |- (Rel Cat /\ Rel dom Cat /\ Rel ran Cat )
5		11st22nd 14348	. . . 4 |- (((Rel Cat /\ Rel dom Cat /\ Rel ran Cat ) /\ T e. Cat ) -> T = <.<.(1st` (1st` T)), (2nd` (1st` T))>., <.(1st` (2nd` T)), (2nd` (2nd` T))>.>.)
6	4, 5	mpan 759	. . 3 |- (T e. Cat -> T = <.<.(1st` (1st` T)), (2nd` (1st` T))>., <.(1st` (2nd` T)), (2nd` (2nd` T))>.>.)
7		eqid 1884	. . . . . 6 |- (dom` T) = (dom` T)
8	7	domval 15070	. . . . 5 |- (dom` T) = (1st` (1st` T))
9		eqid 1884	. . . . . 6 |- (cod` T) = (cod` T)
10	9	codval 15071	. . . . 5 |- (cod` T) = (2nd` (1st` T))
11	8, 10	opeq12i 3163	. . . 4 |- <.(dom` T), (cod` T)>. = <.(1st` (1st` T)), (2nd` (1st` T))>.
12		eqid 1884	. . . . . 6 |- (id` T) = (id` T)
13	12	idval 15072	. . . . 5 |- (id` T) = (1st` (2nd` T))
14		eqid 1884	. . . . . 6 |- (o` T) = (o` T)
15	14	cmpval 15073	. . . . 5 |- (o` T) = (2nd` (2nd` T))
16	13, 15	opeq12i 3163	. . . 4 |- <.(id` T), (o` T)>. = <.(1st` (2nd` T)), (2nd` (2nd` T))>.
17	11, 16	opeq12i 3163	. . 3 |- <.<.(dom` T), (cod` T)>., <.(id` T), (o` T)>.>. = <.<.(1st` (1st` T)), (2nd` (1st` T))>., <.(1st` (2nd` T)), (2nd` (2nd` T))>.>.
18	6, 17	syl6eqr 1946	. 2 |- (T e. Cat -> T = <.<.(dom` T), (cod` T)>., <.(id` T), (o` T)>.>.)
19		eqid 1884	. . . . 5 |- dom (dom` T) = dom (dom` T)
20		eqid 1884	. . . . 5 |- dom (id` T) = dom (id` T)
21	7, 9, 12, 14, 19, 20	cati 15102	. . . 4 |- (T e. Cat -> ((<.<.(dom` T), (cod` T)>., <.(id` T), (o` T)>.>. e. Ded /\ A.x e. dom (dom` T)A.y e. dom (dom` T)A.z e. dom (dom` T)((((dom` T)` z) = ((cod` T)` y) /\ ((dom` T)` y) = ((cod` T)` x)) -> (z(o` T)(y(o` T)x)) = ((z(o` T)y)(o` T)x))) /\ (A.w e. dom (id` T)A.x e. dom (dom` T)(((cod` T)` x) = w -> (((id` T)` w)(o` T)x) = x) /\ A.w e. dom (id` T)A.x e. dom (dom` T)(((dom` T)` x) = w -> (x(o` T)((id` T)` w)) = x))))
22	21	simplld 348	. . 3 |- (T e. Cat -> (<.<.(dom` T), (cod` T)>., <.(id` T), (o` T)>.>. e. Ded /\ A.x e. dom (dom` T)A.y e. dom (dom` T)A.z e. dom (dom` T)((((dom` T)` z) = ((cod` T)` y) /\ ((dom` T)` y) = ((cod` T)` x)) -> (z(o` T)(y(o` T)x)) = ((z(o` T)y)(o` T)x))))
23	22	simplld 348	. 2 |- (T e. Cat -> <.<.(dom` T), (cod` T)>., <.(id` T), (o` T)>.>. e. Ded )
24	18, 23	eqeltrd 1971	1 |- (T e. Cat -> T e. Ded )

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  <.cop 3046  dom cdm 3986  ran crn 3987  Rel wrel 3991  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062   Ded cded 15081   Cat ccat 15099

This theorem is referenced by:  domc 15112  codc 15113  idc 15114  cmppfc 15115  idosc 15116  cmppfcd 15117  domcmpc 15118  codcmpc 15119  dualcat2 15133  mrdmcd 15143  eqidob 15144  homib 15145  homgrf 15151  idsubidsup 15205

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-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-v 2294  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-fo 4012  df-fv 4014  df-opr 4886  df-1st 5020  df-2nd 5021  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-cat 15100

Copyright terms: Public domain