Metamath Proof Explorer

Theorem uobeq3

Description: An isomorphism between categories generates equal sets of universal objects. (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 )
uobeq3.i 
|- I = ( Iso ` Q )
uobeq3.1 
|- ( ph -> K e. ( D I E ) )
Assertion uobeq3 
|- ( 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 uobeq3.i 
 |-  I = ( Iso ` Q )
8 uobeq3.1 
 |-  ( ph -> K e. ( D I E ) )
9 eqid 
 |-  ( Sect ` Q ) = ( Sect ` Q )
10 eqid 
 |-  ( Base ` E ) = ( Base ` E )
11 6 1 10 7 8 catcisoi 
 |-  ( ph -> ( K e. ( ( D Full E ) i^i ( D Faith E ) ) /\ ( 1st ` K ) : B -1-1-onto-> ( Base ` E ) ) )
12 11 simpld 
 |-  ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
13 12 elin1d 
 |-  ( ph -> K e. ( D Full E ) )
14 eqid 
 |-  ( Inv ` Q ) = ( Inv ` Q )
15 14 7 isoval2 
 |-  ( D I E ) = dom ( D ( Inv ` Q ) E )
16 8 15 eleqtrdi 
 |-  ( ph -> K e. dom ( D ( Inv ` Q ) E ) )
17 eldmg 
 |-  ( K e. dom ( D ( Inv ` Q ) E ) -> ( K e. dom ( D ( Inv ` Q ) E ) <-> E. l K ( D ( Inv ` Q ) E ) l ) )
18 17 ibi 
 |-  ( K e. dom ( D ( Inv ` Q ) E ) -> E. l K ( D ( Inv ` Q ) E ) l )
19 14 9 isinv2 
 |-  ( K ( D ( Inv ` Q ) E ) l <-> ( K ( D ( Sect ` Q ) E ) l /\ l ( E ( Sect ` Q ) D ) K ) )
20 19 simplbi 
 |-  ( K ( D ( Inv ` Q ) E ) l -> K ( D ( Sect ` Q ) E ) l )
21 20 eximi 
 |-  ( E. l K ( D ( Inv ` Q ) E ) l -> E. l K ( D ( Sect ` Q ) E ) l )
22 16 18 21 3syl 
 |-  ( ph -> E. l K ( D ( Sect ` Q ) E ) l )
23 eldmg 
 |-  ( K e. ( D I E ) -> ( K e. dom ( D ( Sect ` Q ) E ) <-> E. l K ( D ( Sect ` Q ) E ) l ) )
24 8 23 syl 
 |-  ( ph -> ( K e. dom ( D ( Sect ` Q ) E ) <-> E. l K ( D ( Sect ` Q ) E ) l ) )
25 22 24 mpbird 
 |-  ( ph -> K e. dom ( D ( Sect ` Q ) E ) )
26 1 2 3 4 5 6 9 13 25 uobeq2 
 |-  ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )