Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  catpropd Structured version   Unicode version

Theorem catpropd 13927
 Description: Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypotheses
Ref Expression
catpropd.1 f f
catpropd.2 compf compf
catpropd.3
catpropd.4
Assertion
Ref Expression
catpropd

Proof of Theorem catpropd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 444 . . . . . . . . . . 11 comp comp comp comp comp comp
21ralimi 2773 . . . . . . . . . 10 comp comp comp comp comp comp
32ralimi 2773 . . . . . . . . 9 comp comp comp comp comp comp
43ralimi 2773 . . . . . . . 8 comp comp comp comp comp comp
54ralimi 2773 . . . . . . 7 comp comp comp comp comp comp
65adantl 453 . . . . . 6 comp comp comp comp comp comp comp comp
76ralimi 2773 . . . . 5 comp comp comp comp comp comp comp comp
87a1i 11 . . . 4 comp comp comp comp comp comp comp comp
9 simpl 444 . . . . . . . . . . 11 comp comp comp comp comp comp
109ralimi 2773 . . . . . . . . . 10 comp comp comp comp comp comp
1110ralimi 2773 . . . . . . . . 9 comp comp comp comp comp comp
1211ralimi 2773 . . . . . . . 8 comp comp comp comp comp comp
1312ralimi 2773 . . . . . . 7 comp comp comp comp comp comp
1413adantl 453 . . . . . 6 comp comp comp comp comp comp comp comp
1514ralimi 2773 . . . . 5 comp comp comp comp comp comp comp comp
1615a1i 11 . . . 4 comp comp comp comp comp comp comp comp
17 nfra1 2748 . . . . . . . 8 comp
18 nfv 1629 . . . . . . . 8 comp
19 nfra1 2748 . . . . . . . . . 10 comp
20 nfv 1629 . . . . . . . . . 10 comp
21 nfra1 2748 . . . . . . . . . . . . . 14 comp
22 nfv 1629 . . . . . . . . . . . . . 14 comp
23 oveq1 6080 . . . . . . . . . . . . . . . . 17 comp comp
2423eleq1d 2501 . . . . . . . . . . . . . . . 16 comp comp
2524cbvralv 2924 . . . . . . . . . . . . . . 15 comp comp
26 oveq2 6081 . . . . . . . . . . . . . . . . 17 comp comp
2726eleq1d 2501 . . . . . . . . . . . . . . . 16 comp comp
2827ralbidv 2717 . . . . . . . . . . . . . . 15 comp comp
2925, 28syl5bb 249 . . . . . . . . . . . . . 14 comp comp
3021, 22, 29cbvral 2920 . . . . . . . . . . . . 13 comp comp
31 oveq2 6081 . . . . . . . . . . . . . . 15
32 oveq2 6081 . . . . . . . . . . . . . . . . 17 comp comp
3332oveqd 6090 . . . . . . . . . . . . . . . 16 comp comp
34 oveq2 6081 . . . . . . . . . . . . . . . 16
3533, 34eleq12d 2503 . . . . . . . . . . . . . . 15 comp comp
3631, 35raleqbidv 2908 . . . . . . . . . . . . . 14 comp comp
3736ralbidv 2717 . . . . . . . . . . . . 13 comp comp
3830, 37syl5bb 249 . . . . . . . . . . . 12 comp comp
3938cbvralv 2924 . . . . . . . . . . 11 comp comp
40 oveq2 6081 . . . . . . . . . . . . 13
41 oveq1 6080 . . . . . . . . . . . . . 14
42 opeq2 3977 . . . . . . . . . . . . . . . . 17
4342oveq1d 6088 . . . . . . . . . . . . . . . 16 comp comp
4443oveqd 6090 . . . . . . . . . . . . . . 15 comp comp
4544eleq1d 2501 . . . . . . . . . . . . . 14 comp comp
4641, 45raleqbidv 2908 . . . . . . . . . . . . 13 comp comp
4740, 46raleqbidv 2908 . . . . . . . . . . . 12 comp comp
4847ralbidv 2717 . . . . . . . . . . 11 comp comp
4939, 48syl5bb 249 . . . . . . . . . 10 comp comp
5019, 20, 49cbvral 2920 . . . . . . . . 9 comp comp
51 oveq1 6080 . . . . . . . . . . . . 13
52 opeq1 3976 . . . . . . . . . . . . . . . . 17
5352oveq1d 6088 . . . . . . . . . . . . . . . 16 comp comp
5453oveqd 6090 . . . . . . . . . . . . . . 15 comp comp
55 oveq1 6080 . . . . . . . . . . . . . . 15
5654, 55eleq12d 2503 . . . . . . . . . . . . . 14 comp comp
5756ralbidv 2717 . . . . . . . . . . . . 13 comp comp
5851, 57raleqbidv 2908 . . . . . . . . . . . 12 comp comp
5958ralbidv 2717 . . . . . . . . . . 11 comp comp
60 ralcom 2860 . . . . . . . . . . 11 comp comp
6159, 60syl6bb 253 . . . . . . . . . 10 comp comp
6261ralbidv 2717 . . . . . . . . 9 comp comp
6350, 62syl5bb 249 . . . . . . . 8 comp comp
6417, 18, 63cbvral 2920 . . . . . . 7 comp comp
6564biimpi 187 . . . . . 6 comp comp
6665ancri 536 . . . . 5 comp comp comp
67 r19.26 2830 . . . . . . . . . . . 12 comp comp comp comp
68 r19.26 2830 . . . . . . . . . . . . . . 15 comp comp comp comp
69 r19.26 2830 . . . . . . . . . . . . . . . . . . . . . . . 24 comp comp comp comp
70 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
71 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
72 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
73 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
74 catpropd.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 f f
7574adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 f f
7675ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 f f
7776ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp f f
78 catpropd.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 compf compf
7978ad5antr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 compf compf
8079ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp compf compf
81 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
8281ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8382ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
84 simp-4r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8584ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
86 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
87 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8887ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
89 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp comp
9070, 71, 72, 73, 77, 80, 83, 85, 86, 88, 89comfeqval 13926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 comp comp comp comp comp comp
91 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9291ad4antr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
93 simp-4r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp comp
94 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
9570, 71, 72, 73, 77, 80, 83, 92, 86, 93, 94comfeqval 13926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 comp comp comp comp comp comp
9690, 95eqeq12d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 comp comp comp comp comp comp comp comp comp comp
9796ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 comp comp comp comp comp comp comp comp comp comp
9897ralimdva 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 comp comp comp comp comp comp comp comp comp comp
99 ralbi 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp
10098, 99syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 comp comp comp comp comp comp comp comp comp comp
101100ralimdva 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 comp comp comp comp comp comp comp comp comp comp
102101impancom 428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 comp comp comp comp comp comp comp comp comp comp
103102impr 603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 comp comp comp comp comp comp comp comp comp comp
104 ralbi 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 comp comp comp comp comp comp comp comp comp comp
106105anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 comp comp comp comp comp comp comp comp comp comp comp comp
107106ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25 comp comp comp comp comp comp comp comp comp comp comp comp
108107ralimdva 2776 . . . . . . . . . . . . . . . . . . . . . . . 24 comp comp comp comp comp comp comp comp comp comp comp comp
10969, 108syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . 23 comp comp comp comp comp comp comp comp comp comp comp comp
110109expdimp 427 . . . . . . . . . . . . . . . . . . . . . 22 comp comp comp comp comp comp comp comp comp comp comp comp
111 ralbi 2834 . . . . . . . . . . . . . . . . . . . . . 22 comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp
112110, 111syl6 31 . . . . . . . . . . . . . . . . . . . . 21 comp comp comp comp comp comp comp comp comp comp comp comp
113112an32s 780 . . . . . . . . . . . . . . . . . . . 20 comp comp comp comp comp comp comp comp comp comp comp comp
114113ralimdva 2776 . . . . . . . . . . . . . . . . . . 19 comp comp