Metamath Proof Explorer

Theorem par2diag

Description: Two constant functors into the concrete parallel-arrow category and a natural transformation whose component is the empty-set arrow. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses par2diag.c 
|- C = ( SetCat ` 1o )
par2diag.e 
|- E = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
par2diag.l 
|- L = ( E DiagFunc C )
par2diag.f 
|- F = ( ( 1st ` L ) ` (/) )
par2diag.g 
|- G = ( ( 1st ` L ) ` 1o )
par2diag.a 
|- A = ( 1o X. { (/) } )
Assertion par2diag 
|- ( ( F e. ( C Func E ) /\ G e. ( C Func E ) ) /\ ( A e. ( F ( C Nat E ) G ) /\ ( A ` (/) ) = (/) ) /\ ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o ) )

Proof

Step Hyp Ref Expression
1 par2diag.c 
 |-  C = ( SetCat ` 1o )
2 par2diag.e 
 |-  E = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
3 par2diag.l 
 |-  L = ( E DiagFunc C )
4 par2diag.f 
 |-  F = ( ( 1st ` L ) ` (/) )
5 par2diag.g 
 |-  G = ( ( 1st ` L ) ` 1o )
6 par2diag.a 
 |-  A = ( 1o X. { (/) } )
7 2 par2catid 
 |-  ( E e. Cat /\ ( Id ` E ) = ( y e. 2o |-> 2o ) )
8 7 simpli 
 |-  E e. Cat
9 8 a1i 
 |-  ( T. -> E e. Cat )
10 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
11 1 10 eqeltri 
 |-  C e. TermCat
12 11 a1i 
 |-  ( T. -> C e. TermCat )
13 12 termccatd 
 |-  ( T. -> C e. Cat )
14 2 par2str 
 |-  ( 2o = ( Base ` E ) /\ ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` E ) /\ ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) = ( comp ` E ) )
15 14 simp1i 
 |-  2o = ( Base ` E )
16 0ex 
 |-  (/) e. _V
17 16 prid1 
 |-  (/) e. { (/) , 1o }
18 df2o3 
 |-  2o = { (/) , 1o }
19 17 18 eleqtrri 
 |-  (/) e. 2o
20 19 a1i 
 |-  ( T. -> (/) e. 2o )
21 3 9 13 15 20 4 diag1cl 
 |-  ( T. -> F e. ( C Func E ) )
22 1oelpr 
 |-  1o e. { (/) , 1o }
23 22 18 eleqtrri 
 |-  1o e. 2o
24 23 a1i 
 |-  ( T. -> 1o e. 2o )
25 3 9 13 15 24 5 diag1cl 
 |-  ( T. -> G e. ( C Func E ) )
26 21 25 jca 
 |-  ( T. -> ( F e. ( C Func E ) /\ G e. ( C Func E ) ) )
27 1 setc1obas 
 |-  1o = ( Base ` C )
28 14 simp2i 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( Hom ` E )
29 eqid 
 |-  ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) = ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) )
30 29 par2hom 
 |-  ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = { 2o } /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = { 2o } /\ ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = (/) ) )
31 30 simp3i 
 |-  ( ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o /\ ( 1o ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) (/) ) = (/) )
32 31 simpli 
 |-  ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) = 2o
33 19 32 eleqtrri 
 |-  (/) e. ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o )
34 33 a1i 
 |-  ( T. -> (/) e. ( (/) ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) 1o ) )
35 eqid 
 |-  ( C Nat E ) = ( C Nat E )
36 3 15 27 28 9 13 20 24 34 35 diag2cl 
 |-  ( T. -> ( 1o X. { (/) } ) e. ( ( ( 1st ` L ) ` (/) ) ( C Nat E ) ( ( 1st ` L ) ` 1o ) ) )
37 4 5 oveq12i 
 |-  ( F ( C Nat E ) G ) = ( ( ( 1st ` L ) ` (/) ) ( C Nat E ) ( ( 1st ` L ) ` 1o ) )
38 36 6 37 3eltr4g 
 |-  ( T. -> A e. ( F ( C Nat E ) G ) )
39 6 fveq1i 
 |-  ( A ` (/) ) = ( ( 1o X. { (/) } ) ` (/) )
40 0lt1o 
 |-  (/) e. 1o
41 16 fvconst2 
 |-  ( (/) e. 1o -> ( ( 1o X. { (/) } ) ` (/) ) = (/) )
42 40 41 ax-mp 
 |-  ( ( 1o X. { (/) } ) ` (/) ) = (/)
43 39 42 eqtri 
 |-  ( A ` (/) ) = (/)
44 38 43 jctir 
 |-  ( T. -> ( A e. ( F ( C Nat E ) G ) /\ ( A ` (/) ) = (/) ) )
45 40 a1i 
 |-  ( T. -> (/) e. 1o )
46 3 9 13 15 20 4 27 45 diag11 
 |-  ( T. -> ( ( 1st ` F ) ` (/) ) = (/) )
47 3 9 13 15 24 5 27 45 diag11 
 |-  ( T. -> ( ( 1st ` G ) ` (/) ) = 1o )
48 46 47 jca 
 |-  ( T. -> ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o ) )
49 26 44 48 3jca 
 |-  ( T. -> ( ( F e. ( C Func E ) /\ G e. ( C Func E ) ) /\ ( A e. ( F ( C Nat E ) G ) /\ ( A ` (/) ) = (/) ) /\ ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o ) ) )
50 49 mptru 
 |-  ( ( F e. ( C Func E ) /\ G e. ( C Func E ) ) /\ ( A e. ( F ( C Nat E ) G ) /\ ( A ` (/) ) = (/) ) /\ ( ( ( 1st ` F ) ` (/) ) = (/) /\ ( ( 1st ` G ) ` (/) ) = 1o ) )