Metamath Proof Explorer

Theorem uobeq

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

Ref Expression
Hypotheses uobeq.b 
|- B = ( Base ` D )
uobeq.i 
|- I = ( idFunc ` D )
uobeq.x 
|- ( ph -> X e. B )
uobeq.f 
|- ( ph -> F e. ( C Func D ) )
uobeq.k 
|- ( ph -> K e. ( D Full E ) )
uobeq.g 
|- ( ph -> ( K o.func F ) = G )
uobeq.y 
|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
uobeq.n 
|- ( ph -> ( L o.func K ) = I )
uobeq.l 
|- ( ph -> L e. ( E Func D ) )
Assertion uobeq 
|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Proof

Step Hyp Ref Expression
1 uobeq.b 
 |-  B = ( Base ` D )
2 uobeq.i 
 |-  I = ( idFunc ` D )
3 uobeq.x 
 |-  ( ph -> X e. B )
4 uobeq.f 
 |-  ( ph -> F e. ( C Func D ) )
5 uobeq.k 
 |-  ( ph -> K e. ( D Full E ) )
6 uobeq.g 
 |-  ( ph -> ( K o.func F ) = G )
7 uobeq.y 
 |-  ( ph -> ( ( 1st ` K ) ` X ) = Y )
8 uobeq.n 
 |-  ( ph -> ( L o.func K ) = I )
9 uobeq.l 
 |-  ( ph -> L e. ( E Func D ) )
10 19.42v 
 |-  ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) <-> ( ph /\ E. m z ( F ( C UP D ) X ) m ) )
11 fvexd 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) e. _V )
12 7 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( 1st ` K ) ` X ) = Y )
13 relfunc 
 |-  Rel ( D Func E )
14 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
15 14 5 sselid 
 |-  ( ph -> K e. ( D Func E ) )
16 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
17 13 15 16 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
18 15 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
19 9 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( E Func D ) ( 2nd ` L ) )
20 15 9 cofu1st2nd 
 |-  ( ph -> ( L o.func K ) = ( <. ( 1st ` L ) , ( 2nd ` L ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
21 20 8 eqtr3d 
 |-  ( ph -> ( <. ( 1st ` L ) , ( 2nd ` L ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) = I )
22 2 18 19 21 cofidfth 
 |-  ( ph -> ( 1st ` K ) ( D Faith E ) ( 2nd ` K ) )
23 df-br 
 |-  ( ( 1st ` K ) ( D Faith E ) ( 2nd ` K ) <-> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Faith E ) )
24 22 23 sylib 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Faith E ) )
25 17 24 eqeltrd 
 |-  ( ph -> K e. ( D Faith E ) )
26 5 25 elind 
 |-  ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
27 26 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
28 6 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( K o.func F ) = G )
29 eqidd 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) )
30 simpr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( F ( C UP D ) X ) m )
31 12 27 28 29 30 uptrai 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( G ( C UP E ) Y ) ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) )
32 breq2 
 |-  ( n = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) -> ( z ( G ( C UP E ) Y ) n <-> z ( G ( C UP E ) Y ) ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) ) )
33 11 31 32 spcedv 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
34 33 exlimiv 
 |-  ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
35 10 34 sylbir 
 |-  ( ( ph /\ E. m z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
36 19.42v 
 |-  ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) <-> ( ph /\ E. n z ( G ( C UP E ) Y ) n ) )
37 fvexd 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) e. _V )
38 7 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` K ) ` X ) = Y )
39 26 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
40 6 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( K o.func F ) = G )
41 3 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> X e. B )
42 4 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> F e. ( C Func D ) )
43 eqidd 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) = ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) )
44 simpr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( G ( C UP E ) Y ) n )
45 38 39 40 1 41 42 43 44 uptrar 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) )
46 breq2 
 |-  ( m = ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) -> ( z ( F ( C UP D ) X ) m <-> z ( F ( C UP D ) X ) ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) ) )
47 37 45 46 spcedv 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
48 47 exlimiv 
 |-  ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
49 36 48 sylbir 
 |-  ( ( ph /\ E. n z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
50 35 49 impbida 
 |-  ( ph -> ( E. m z ( F ( C UP D ) X ) m <-> E. n z ( G ( C UP E ) Y ) n ) )
51 relup 
 |-  Rel ( F ( C UP D ) X )
52 releldmb 
 |-  ( Rel ( F ( C UP D ) X ) -> ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) )
53 51 52 ax-mp 
 |-  ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m )
54 relup 
 |-  Rel ( G ( C UP E ) Y )
55 releldmb 
 |-  ( Rel ( G ( C UP E ) Y ) -> ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) )
56 54 55 ax-mp 
 |-  ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n )
57 50 53 56 3bitr4g 
 |-  ( ph -> ( z e. dom ( F ( C UP D ) X ) <-> z e. dom ( G ( C UP E ) Y ) ) )
58 57 eqrdv 
 |-  ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )