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

Metamath Proof Explorer

Theorem uobeqw

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

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

Proof

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