This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcsetc1o

Description: Value of the functor to the trivial category. The converse is also true because F would be the empty set if C were not a category; and the empty set cannot equal an ordered pair of two sets. (Contributed by Zhi Wang, 22-Oct-2025)

Ref Expression
Hypotheses funcsetc1o.1 
|- .1. = ( SetCat ` 1o )
funcsetc1o.f 
|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
funcsetc1o.c 
|- ( ph -> C e. Cat )
funcsetc1o.b 
|- B = ( Base ` C )
funcsetc1o.h 
|- H = ( Hom ` C )
Assertion funcsetc1o 
|- ( ph -> F = <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. )

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 
 |-  .1. = ( SetCat ` 1o )
2 funcsetc1o.f 
 |-  F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
3 funcsetc1o.c 
 |-  ( ph -> C e. Cat )
4 funcsetc1o.b 
 |-  B = ( Base ` C )
5 funcsetc1o.h 
 |-  H = ( Hom ` C )
6 eqid 
 |-  ( .1. DiagFunc C ) = ( .1. DiagFunc C )
7 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
8 1 7 eqeltri 
 |-  .1. e. TermCat
9 8 a1i 
 |-  ( ph -> .1. e. TermCat )
10 9 termccd 
 |-  ( ph -> .1. e. Cat )
11 1 setc1obas 
 |-  1o = ( Base ` .1. )
12 0lt1o 
 |-  (/) e. 1o
13 12 a1i 
 |-  ( ph -> (/) e. 1o )
14 eqid 
 |-  ( Id ` .1. ) = ( Id ` .1. )
15 6 10 3 11 13 2 4 5 14 diag1a 
 |-  ( ph -> F = <. ( B X. { (/) } ) , ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) ) >. )
16 df1o2 
 |-  1o = { (/) }
17 16 xpeq2i 
 |-  ( B X. 1o ) = ( B X. { (/) } )
18 1 14 setc1oid 
 |-  ( ( Id ` .1. ) ` (/) ) = (/)
19 18 sneqi 
 |-  { ( ( Id ` .1. ) ` (/) ) } = { (/) }
20 16 19 eqtr4i 
 |-  1o = { ( ( Id ` .1. ) ` (/) ) }
21 20 xpeq2i 
 |-  ( ( x H y ) X. 1o ) = ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } )
22 21 a1i 
 |-  ( ( x e. B /\ y e. B ) -> ( ( x H y ) X. 1o ) = ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) )
23 22 mpoeq3ia 
 |-  ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) = ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) )
24 17 23 opeq12i 
 |-  <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. = <. ( B X. { (/) } ) , ( x e. B , y e. B |-> ( ( x H y ) X. { ( ( Id ` .1. ) ` (/) ) } ) ) >.
25 15 24 eqtr4di 
 |-  ( ph -> F = <. ( B X. 1o ) , ( x e. B , y e. B |-> ( ( x H y ) X. 1o ) ) >. )