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

Metamath Proof Explorer

Theorem uobeq2

Description: If a full functor (in fact, a full embedding) is a section, then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses uobeq2.b 
|- B = ( Base ` D )
uobeq2.x 
|- ( ph -> X e. B )
uobeq2.f 
|- ( ph -> F e. ( C Func D ) )
uobeq2.g 
|- ( ph -> ( K o.func F ) = G )
uobeq2.y 
|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
uobeq2.q 
|- Q = ( CatCat ` U )
uobeq2.s 
|- S = ( Sect ` Q )
uobeq2.k 
|- ( ph -> K e. ( D Full E ) )
uobeq2.1 
|- ( ph -> K e. dom ( D S E ) )
Assertion uobeq2 
|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Proof

Step Hyp Ref Expression
1 uobeq2.b 
 |-  B = ( Base ` D )
2 uobeq2.x 
 |-  ( ph -> X e. B )
3 uobeq2.f 
 |-  ( ph -> F e. ( C Func D ) )
4 uobeq2.g 
 |-  ( ph -> ( K o.func F ) = G )
5 uobeq2.y 
 |-  ( ph -> ( ( 1st ` K ) ` X ) = Y )
6 uobeq2.q 
 |-  Q = ( CatCat ` U )
7 uobeq2.s 
 |-  S = ( Sect ` Q )
8 uobeq2.k 
 |-  ( ph -> K e. ( D Full E ) )
9 uobeq2.1 
 |-  ( ph -> K e. dom ( D S E ) )
10 eldmg 
 |-  ( K e. dom ( D S E ) -> ( K e. dom ( D S E ) <-> E. l K ( D S E ) l ) )
11 10 ibi 
 |-  ( K e. dom ( D S E ) -> E. l K ( D S E ) l )
12 9 11 syl 
 |-  ( ph -> E. l K ( D S E ) l )
13 2 adantr 
 |-  ( ( ph /\ K ( D S E ) l ) -> X e. B )
14 3 adantr 
 |-  ( ( ph /\ K ( D S E ) l ) -> F e. ( C Func D ) )
15 4 adantr 
 |-  ( ( ph /\ K ( D S E ) l ) -> ( K o.func F ) = G )
16 5 adantr 
 |-  ( ( ph /\ K ( D S E ) l ) -> ( ( 1st ` K ) ` X ) = Y )
17 eqid 
 |-  ( idFunc ` D ) = ( idFunc ` D )
18 8 adantr 
 |-  ( ( ph /\ K ( D S E ) l ) -> K e. ( D Full E ) )
19 eqid 
 |-  ( Hom ` Q ) = ( Hom ` Q )
20 6 19 17 7 catcsect 
 |-  ( K ( D S E ) l <-> ( ( K e. ( D ( Hom ` Q ) E ) /\ l e. ( E ( Hom ` Q ) D ) ) /\ ( l o.func K ) = ( idFunc ` D ) ) )
21 20 simprbi 
 |-  ( K ( D S E ) l -> ( l o.func K ) = ( idFunc ` D ) )
22 21 adantl 
 |-  ( ( ph /\ K ( D S E ) l ) -> ( l o.func K ) = ( idFunc ` D ) )
23 20 simplbi 
 |-  ( K ( D S E ) l -> ( K e. ( D ( Hom ` Q ) E ) /\ l e. ( E ( Hom ` Q ) D ) ) )
24 23 simprd 
 |-  ( K ( D S E ) l -> l e. ( E ( Hom ` Q ) D ) )
25 6 19 24 elcatchom 
 |-  ( K ( D S E ) l -> l e. ( E Func D ) )
26 25 adantl 
 |-  ( ( ph /\ K ( D S E ) l ) -> l e. ( E Func D ) )
27 1 13 14 15 16 17 18 22 26 uobeq 
 |-  ( ( ph /\ K ( D S E ) l ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )
28 12 27 exlimddv 
 |-  ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )