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

Metamath Proof Explorer

Theorem eufunc

Description: If there exists a unique functor from a non-empty category, then the base of the target category is 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 eufunc 
|- ( ph -> E! x x e. B )

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 euex 
 |-  ( E! f f e. ( C Func D ) -> E. f f e. ( C Func D ) )
6 simpr 
 |-  ( ( f e. ( C Func D ) /\ B = (/) ) -> B = (/) )
7 simpl 
 |-  ( ( f e. ( C Func D ) /\ B = (/) ) -> f e. ( C Func D ) )
8 2 4 6 7 func0g2 
 |-  ( ( f e. ( C Func D ) /\ B = (/) ) -> A = (/) )
9 8 ex 
 |-  ( f e. ( C Func D ) -> ( B = (/) -> A = (/) ) )
10 9 exlimiv 
 |-  ( E. f f e. ( C Func D ) -> ( B = (/) -> A = (/) ) )
11 1 5 10 3syl 
 |-  ( ph -> ( B = (/) -> A = (/) ) )
12 11 imp 
 |-  ( ( ph /\ B = (/) ) -> A = (/) )
13 3 12 mteqand 
 |-  ( ph -> B =/= (/) )
14 n0 
 |-  ( B =/= (/) <-> E. x x e. B )
15 13 14 sylib 
 |-  ( ph -> E. x x e. B )
16 1 2 3 4 eufunclem 
 |-  ( ph -> B ~<_ 1o )
17 modom2 
 |-  ( E* x x e. B <-> B ~<_ 1o )
18 16 17 sylibr 
 |-  ( ph -> E* x x e. B )
19 df-eu 
 |-  ( E! x x e. B <-> ( E. x x e. B /\ E* x x e. B ) )
20 15 18 19 sylanbrc 
 |-  ( ph -> E! x x e. B )