Theorem uobeq3

Description: An isomorphism between categories generates equal sets of universal objects. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobeq2.b	|- B = ( Base ` D )
	uobeq2.x	|- ( ph -> X e. B )
	uobeq2.f	|- ( ph -> F e. ( C Func D ) )
	uobeq2.g	|- ( ph -> ( K o.func F ) = G )
	uobeq2.y	|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
	uobeq2.q	|- Q = ( CatCat ` U )
	uobeq3.i	|- I = ( Iso ` Q )
	uobeq3.1	|- ( ph -> K e. ( D I E ) )
Assertion	uobeq3	|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		uobeq2.b	|- B = ( Base ` D )
2		uobeq2.x	|- ( ph -> X e. B )
3		uobeq2.f	|- ( ph -> F e. ( C Func D ) )
4		uobeq2.g	|- ( ph -> ( K o.func F ) = G )
5		uobeq2.y	|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
6		uobeq2.q	|- Q = ( CatCat ` U )
7		uobeq3.i	|- I = ( Iso ` Q )
8		uobeq3.1	|- ( ph -> K e. ( D I E ) )
9		eqid	|- ( Base ` E ) = ( Base ` E )
10	6 1 9 7 8	catcisoi	|- ( ph -> ( K e. ( ( D Full E ) i^i ( D Faith E ) ) /\ ( 1st ` K ) : B -1-1-onto-> ( Base ` E ) ) )
11	10	simpld	|- ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
12	1 2 3 4 5 11	uobffth	|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )