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

Metamath Proof Explorer

Theorem uobffth

Description: A fully faithful functor generates equal sets of universal objects. (Contributed by Zhi Wang, 19-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 )
uobffth.k 
|- ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
Assertion uobffth 
|- ( 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 uobffth.k 
 |-  ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
7 19.42v 
 |-  ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) <-> ( ph /\ E. m z ( F ( C UP D ) X ) m ) )
8 fvexd 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) e. _V )
9 5 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( 1st ` K ) ` X ) = Y )
10 6 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
11 4 adantr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( K o.func F ) = G )
12 eqidd 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) )
13 simpr 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( F ( C UP D ) X ) m )
14 9 10 11 12 13 uptrai 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( G ( C UP E ) Y ) ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) )
15 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 ) ) )
16 8 14 15 spcedv 
 |-  ( ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
17 16 exlimiv 
 |-  ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
18 7 17 sylbir 
 |-  ( ( ph /\ E. m z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n )
19 19.42v 
 |-  ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) <-> ( ph /\ E. n z ( G ( C UP E ) Y ) n ) )
20 fvexd 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) e. _V )
21 5 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` K ) ` X ) = Y )
22 6 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
23 4 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( K o.func F ) = G )
24 2 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> X e. B )
25 3 adantr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> F e. ( C Func D ) )
26 eqidd 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) = ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) )
27 simpr 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( G ( C UP E ) Y ) n )
28 21 22 23 1 24 25 26 27 uptrar 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) )
29 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 ) ) )
30 20 28 29 spcedv 
 |-  ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
31 30 exlimiv 
 |-  ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
32 19 31 sylbir 
 |-  ( ( ph /\ E. n z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m )
33 18 32 impbida 
 |-  ( ph -> ( E. m z ( F ( C UP D ) X ) m <-> E. n z ( G ( C UP E ) Y ) n ) )
34 relup 
 |-  Rel ( F ( C UP D ) X )
35 releldmb 
 |-  ( Rel ( F ( C UP D ) X ) -> ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) )
36 34 35 ax-mp 
 |-  ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m )
37 relup 
 |-  Rel ( G ( C UP E ) Y )
38 releldmb 
 |-  ( Rel ( G ( C UP E ) Y ) -> ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) )
39 37 38 ax-mp 
 |-  ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n )
40 33 36 39 3bitr4g 
 |-  ( ph -> ( z e. dom ( F ( C UP D ) X ) <-> z e. dom ( G ( C UP E ) Y ) ) )
41 40 eqrdv 
 |-  ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )