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

Metamath Proof Explorer

Theorem eufunclem

Description: If there exists a unique functor from a non-empty category, then the base of the target category is at most a singleton. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypotheses eufunc.f 
|- ( ph -> E! f f e. ( C Func D ) )
eufunc.a 
|- A = ( Base ` C )
eufunc.0 
|- ( ph -> A =/= (/) )
eufunc.b 
|- B = ( Base ` D )
Assertion eufunclem 
|- ( ph -> B ~<_ 1o )

Proof

Step Hyp Ref Expression
1 eufunc.f 
 |-  ( ph -> E! f f e. ( C Func D ) )
2 eufunc.a 
 |-  A = ( Base ` C )
3 eufunc.0 
 |-  ( ph -> A =/= (/) )
4 eufunc.b 
 |-  B = ( Base ` D )
5 eqid 
 |-  ( D DiagFunc C ) = ( D DiagFunc C )
6 euex 
 |-  ( E! f f e. ( C Func D ) -> E. f f e. ( C Func D ) )
7 1 6 syl 
 |-  ( ph -> E. f f e. ( C Func D ) )
8 relfunc 
 |-  Rel ( C Func D )
9 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ f e. ( C Func D ) ) -> ( 1st ` f ) ( C Func D ) ( 2nd ` f ) )
10 8 9 mpan 
 |-  ( f e. ( C Func D ) -> ( 1st ` f ) ( C Func D ) ( 2nd ` f ) )
11 10 funcrcl3 
 |-  ( f e. ( C Func D ) -> D e. Cat )
12 11 exlimiv 
 |-  ( E. f f e. ( C Func D ) -> D e. Cat )
13 7 12 syl 
 |-  ( ph -> D e. Cat )
14 10 funcrcl2 
 |-  ( f e. ( C Func D ) -> C e. Cat )
15 14 exlimiv 
 |-  ( E. f f e. ( C Func D ) -> C e. Cat )
16 7 15 syl 
 |-  ( ph -> C e. Cat )
17 5 13 16 4 2 3 diag1f1 
 |-  ( ph -> ( 1st ` ( D DiagFunc C ) ) : B -1-1-> ( C Func D ) )
18 ovex 
 |-  ( C Func D ) e. _V
19 18 f1dom 
 |-  ( ( 1st ` ( D DiagFunc C ) ) : B -1-1-> ( C Func D ) -> B ~<_ ( C Func D ) )
20 17 19 syl 
 |-  ( ph -> B ~<_ ( C Func D ) )
21 euen1b 
 |-  ( ( C Func D ) ~~ 1o <-> E! f f e. ( C Func D ) )
22 1 21 sylibr 
 |-  ( ph -> ( C Func D ) ~~ 1o )
23 domentr 
 |-  ( ( B ~<_ ( C Func D ) /\ ( C Func D ) ~~ 1o ) -> B ~<_ 1o )
24 20 22 23 syl2anc 
 |-  ( ph -> B ~<_ 1o )