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={\mathrm{Base}}_D$$
	uobffth.x	$$⊢\phi \to X\in B$$
	uobffth.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobffth.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uobffth.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uobffth.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
Assertion	uobffth	Could not format assertion : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uobffth.b	$$⊢B={\mathrm{Base}}_D$$
2		uobffth.x	$$⊢\phi \to X\in B$$
3		uobffth.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		uobffth.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
5		uobffth.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
6		uobffth.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
7		19.42v	Could not format ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) <-> ( ph /\ E. m z ( F ( C UP D ) X ) m ) ) : No typesetting found for |- ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) <-> ( ph /\ E. m z ( F ( C UP D ) X ) m ) ) with typecode |-
8		fvexd	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) e. _V ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) e. _V ) with typecode |-
9	5	adantr	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( 1st ` K ) ` X ) = Y ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( 1st ` K ) ` X ) = Y ) with typecode |-
10	6	adantr	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) with typecode |-
11	4	adantr	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( K o.func F ) = G ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( K o.func F ) = G ) with typecode |-
12		eqidd	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) ) with typecode |-
13		simpr	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( F ( C UP D ) X ) m ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( F ( C UP D ) X ) m ) with typecode |-
14	9 10 11 12 13	uptrai	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( G ( C UP E ) Y ) ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> z ( G ( C UP E ) Y ) ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` m ) ) with typecode |-
15		breq2	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
16	8 14 15	spcedv	Could not format ( ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) : No typesetting found for |- ( ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) with typecode |-
17	16	exlimiv	Could not format ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) : No typesetting found for |- ( E. m ( ph /\ z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) with typecode |-
18	7 17	sylbir	Could not format ( ( ph /\ E. m z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) : No typesetting found for |- ( ( ph /\ E. m z ( F ( C UP D ) X ) m ) -> E. n z ( G ( C UP E ) Y ) n ) with typecode |-
19		19.42v	Could not format ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) <-> ( ph /\ E. n z ( G ( C UP E ) Y ) n ) ) : No typesetting found for |- ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) <-> ( ph /\ E. n z ( G ( C UP E ) Y ) n ) ) with typecode |-
20		fvexd	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) e. _V ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) e. _V ) with typecode |-
21	5	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` K ) ` X ) = Y ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` K ) ` X ) = Y ) with typecode |-
22	6	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) with typecode |-
23	4	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( K o.func F ) = G ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( K o.func F ) = G ) with typecode |-
24	2	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> X e. B ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> X e. B ) with typecode |-
25	3	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> F e. ( C Func D ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> F e. ( C Func D ) ) with typecode |-
26		eqidd	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) = ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) = ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) ) with typecode |-
27		simpr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( G ( C UP E ) Y ) n ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( G ( C UP E ) Y ) n ) with typecode |-
28	21 22 23 1 24 25 26 27	uptrar	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` z ) ) ` n ) ) with typecode |-
29		breq2	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
30	20 28 29	spcedv	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) with typecode |-
31	30	exlimiv	Could not format ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) : No typesetting found for |- ( E. n ( ph /\ z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) with typecode |-
32	19 31	sylbir	Could not format ( ( ph /\ E. n z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) : No typesetting found for |- ( ( ph /\ E. n z ( G ( C UP E ) Y ) n ) -> E. m z ( F ( C UP D ) X ) m ) with typecode |-
33	18 32	impbida	Could not format ( ph -> ( E. m z ( F ( C UP D ) X ) m <-> E. n z ( G ( C UP E ) Y ) n ) ) : No typesetting found for |- ( ph -> ( E. m z ( F ( C UP D ) X ) m <-> E. n z ( G ( C UP E ) Y ) n ) ) with typecode |-
34		relup	Could not format Rel ( F ( C UP D ) X ) : No typesetting found for |- Rel ( F ( C UP D ) X ) with typecode |-
35		releldmb	Could not format ( Rel ( F ( C UP D ) X ) -> ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) ) : No typesetting found for |- ( Rel ( F ( C UP D ) X ) -> ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) ) with typecode |-
36	34 35	ax-mp	Could not format ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) : No typesetting found for |- ( z e. dom ( F ( C UP D ) X ) <-> E. m z ( F ( C UP D ) X ) m ) with typecode |-
37		relup	Could not format Rel ( G ( C UP E ) Y ) : No typesetting found for |- Rel ( G ( C UP E ) Y ) with typecode |-
38		releldmb	Could not format ( Rel ( G ( C UP E ) Y ) -> ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) ) : No typesetting found for |- ( Rel ( G ( C UP E ) Y ) -> ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) ) with typecode |-
39	37 38	ax-mp	Could not format ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) : No typesetting found for |- ( z e. dom ( G ( C UP E ) Y ) <-> E. n z ( G ( C UP E ) Y ) n ) with typecode |-
40	33 36 39	3bitr4g	Could not format ( ph -> ( z e. dom ( F ( C UP D ) X ) <-> z e. dom ( G ( C UP E ) Y ) ) ) : No typesetting found for |- ( ph -> ( z e. dom ( F ( C UP D ) X ) <-> z e. dom ( G ( C UP E ) Y ) ) ) with typecode |-
41	40	eqrdv	Could not format ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-