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 ) )

Metamath Proof Explorer

Theorem uobffth

Proof