Metamath Proof Explorer


Theorem setcval

Description: Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcval.c C = SetCat U
setcval.u φ U V
setcval.h φ H = x U , y U y x
setcval.o φ · ˙ = v U × U , z U g z 2 nd v , f 2 nd v 1 st v g f
Assertion setcval φ C = Base ndx U Hom ndx H comp ndx · ˙

Proof

Step Hyp Ref Expression
1 setcval.c C = SetCat U
2 setcval.u φ U V
3 setcval.h φ H = x U , y U y x
4 setcval.o φ · ˙ = v U × U , z U g z 2 nd v , f 2 nd v 1 st v g f
5 df-setc SetCat = u V Base ndx u Hom ndx x u , y u y x comp ndx v u × u , z u g z 2 nd v , f 2 nd v 1 st v g f
6 simpr φ u = U u = U
7 6 opeq2d φ u = U Base ndx u = Base ndx U
8 eqidd φ u = U y x = y x
9 6 6 8 mpoeq123dv φ u = U x u , y u y x = x U , y U y x
10 3 adantr φ u = U H = x U , y U y x
11 9 10 eqtr4d φ u = U x u , y u y x = H
12 11 opeq2d φ u = U Hom ndx x u , y u y x = Hom ndx H
13 6 sqxpeqd φ u = U u × u = U × U
14 eqidd φ u = U g z 2 nd v , f 2 nd v 1 st v g f = g z 2 nd v , f 2 nd v 1 st v g f
15 13 6 14 mpoeq123dv φ u = U v u × u , z u g z 2 nd v , f 2 nd v 1 st v g f = v U × U , z U g z 2 nd v , f 2 nd v 1 st v g f
16 4 adantr φ u = U · ˙ = v U × U , z U g z 2 nd v , f 2 nd v 1 st v g f
17 15 16 eqtr4d φ u = U v u × u , z u g z 2 nd v , f 2 nd v 1 st v g f = · ˙
18 17 opeq2d φ u = U comp ndx v u × u , z u g z 2 nd v , f 2 nd v 1 st v g f = comp ndx · ˙
19 7 12 18 tpeq123d φ u = U Base ndx u Hom ndx x u , y u y x comp ndx v u × u , z u g z 2 nd v , f 2 nd v 1 st v g f = Base ndx U Hom ndx H comp ndx · ˙
20 2 elexd φ U V
21 tpex Base ndx U Hom ndx H comp ndx · ˙ V
22 21 a1i φ Base ndx U Hom ndx H comp ndx · ˙ V
23 5 19 20 22 fvmptd2 φ SetCat U = Base ndx U Hom ndx H comp ndx · ˙
24 1 23 eqtrid φ C = Base ndx U Hom ndx H comp ndx · ˙