Metamath Proof Explorer

Theorem setc1ocofval

Description: Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

Ref Expression
Hypothesis funcsetc1o.1 
|- .1. = ( SetCat ` 1o )
Assertion setc1ocofval 
|- { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } = ( comp ` .1. )

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 
 |-  .1. = ( SetCat ` 1o )
2 df-ot 
 |-  <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. = <. <. <. (/) , (/) >. , (/) >. , { <. (/) , (/) , (/) >. } >.
3 2 sneqi 
 |-  { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } = { <. <. <. (/) , (/) >. , (/) >. , { <. (/) , (/) , (/) >. } >. }
4 opex 
 |-  <. (/) , (/) >. e. _V
5 0ex 
 |-  (/) e. _V
6 snex 
 |-  { <. (/) , (/) , (/) >. } e. _V
7 df1o2 
 |-  1o = { (/) }
8 7 fveq2i 
 |-  ( SetCat ` 1o ) = ( SetCat ` { (/) } )
9 1 8 eqtri 
 |-  .1. = ( SetCat ` { (/) } )
10 snex 
 |-  { (/) } e. _V
11 10 a1i 
 |-  ( T. -> { (/) } e. _V )
12 eqid 
 |-  ( comp ` .1. ) = ( comp ` .1. )
13 9 11 12 setccofval 
 |-  ( T. -> ( comp ` .1. ) = ( v e. ( { (/) } X. { (/) } ) , z e. { (/) } |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )
14 13 mptru 
 |-  ( comp ` .1. ) = ( v e. ( { (/) } X. { (/) } ) , z e. { (/) } |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) )
15 5 5 xpsn 
 |-  ( { (/) } X. { (/) } ) = { <. (/) , (/) >. }
16 eqid 
 |-  { (/) } = { (/) }
17 eqid 
 |-  ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) = ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) )
18 15 16 17 mpoeq123i 
 |-  ( v e. ( { (/) } X. { (/) } ) , z e. { (/) } |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) = ( v e. { <. (/) , (/) >. } , z e. { (/) } |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) )
19 14 18 eqtri 
 |-  ( comp ` .1. ) = ( v e. { <. (/) , (/) >. } , z e. { (/) } |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) )
20 5 5 op2ndd 
 |-  ( v = <. (/) , (/) >. -> ( 2nd ` v ) = (/) )
21 20 oveq2d 
 |-  ( v = <. (/) , (/) >. -> ( z ^m ( 2nd ` v ) ) = ( z ^m (/) ) )
22 5 5 op1std 
 |-  ( v = <. (/) , (/) >. -> ( 1st ` v ) = (/) )
23 20 22 oveq12d 
 |-  ( v = <. (/) , (/) >. -> ( ( 2nd ` v ) ^m ( 1st ` v ) ) = ( (/) ^m (/) ) )
24 0map0sn0 
 |-  ( (/) ^m (/) ) = { (/) }
25 23 24 eqtrdi 
 |-  ( v = <. (/) , (/) >. -> ( ( 2nd ` v ) ^m ( 1st ` v ) ) = { (/) } )
26 eqidd 
 |-  ( v = <. (/) , (/) >. -> ( g o. f ) = ( g o. f ) )
27 21 25 26 mpoeq123dv 
 |-  ( v = <. (/) , (/) >. -> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) = ( g e. ( z ^m (/) ) , f e. { (/) } |-> ( g o. f ) ) )
28 oveq1 
 |-  ( z = (/) -> ( z ^m (/) ) = ( (/) ^m (/) ) )
29 28 24 eqtrdi 
 |-  ( z = (/) -> ( z ^m (/) ) = { (/) } )
30 eqidd 
 |-  ( z = (/) -> { (/) } = { (/) } )
31 eqidd 
 |-  ( z = (/) -> ( g o. f ) = ( g o. f ) )
32 29 30 31 mpoeq123dv 
 |-  ( z = (/) -> ( g e. ( z ^m (/) ) , f e. { (/) } |-> ( g o. f ) ) = ( g e. { (/) } , f e. { (/) } |-> ( g o. f ) ) )
33 eqid 
 |-  ( g e. { (/) } , f e. { (/) } |-> ( g o. f ) ) = ( g e. { (/) } , f e. { (/) } |-> ( g o. f ) )
34 coeq1 
 |-  ( g = (/) -> ( g o. f ) = ( (/) o. f ) )
35 co01 
 |-  ( (/) o. f ) = (/)
36 34 35 eqtrdi 
 |-  ( g = (/) -> ( g o. f ) = (/) )
37 eqidd 
 |-  ( f = (/) -> (/) = (/) )
38 33 36 37 mposn 
 |-  ( ( (/) e. _V /\ (/) e. _V /\ (/) e. _V ) -> ( g e. { (/) } , f e. { (/) } |-> ( g o. f ) ) = { <. <. (/) , (/) >. , (/) >. } )
39 5 5 5 38 mp3an 
 |-  ( g e. { (/) } , f e. { (/) } |-> ( g o. f ) ) = { <. <. (/) , (/) >. , (/) >. }
40 32 39 eqtrdi 
 |-  ( z = (/) -> ( g e. ( z ^m (/) ) , f e. { (/) } |-> ( g o. f ) ) = { <. <. (/) , (/) >. , (/) >. } )
41 df-ot 
 |-  <. (/) , (/) , (/) >. = <. <. (/) , (/) >. , (/) >.
42 41 sneqi 
 |-  { <. (/) , (/) , (/) >. } = { <. <. (/) , (/) >. , (/) >. }
43 40 42 eqtr4di 
 |-  ( z = (/) -> ( g e. ( z ^m (/) ) , f e. { (/) } |-> ( g o. f ) ) = { <. (/) , (/) , (/) >. } )
44 19 27 43 mposn 
 |-  ( ( <. (/) , (/) >. e. _V /\ (/) e. _V /\ { <. (/) , (/) , (/) >. } e. _V ) -> ( comp ` .1. ) = { <. <. <. (/) , (/) >. , (/) >. , { <. (/) , (/) , (/) >. } >. } )
45 4 5 6 44 mp3an 
 |-  ( comp ` .1. ) = { <. <. <. (/) , (/) >. , (/) >. , { <. (/) , (/) , (/) >. } >. }
46 3 45 eqtr4i 
 |-  { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } = ( comp ` .1. )