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={\mathrm{Base}}_D$$
	uobeq2.x	$$⊢\phi \to X\in B$$
	uobeq2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobeq2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uobeq2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uobeq2.q	$$⊢Q=\mathrm{CatCat}\left(U\right)$$
	uobeq3.i	$$⊢I=\mathrm{Iso}\left(Q\right)$$
	uobeq3.1	$$⊢\phi \to K\in \left(DIE\right)$$
Assertion	uobeq3	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		uobeq2.b	$$⊢B={\mathrm{Base}}_D$$
2		uobeq2.x	$$⊢\phi \to X\in B$$
3		uobeq2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		uobeq2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
5		uobeq2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
6		uobeq2.q	$$⊢Q=\mathrm{CatCat}\left(U\right)$$
7		uobeq3.i	$$⊢I=\mathrm{Iso}\left(Q\right)$$
8		uobeq3.1	$$⊢\phi \to K\in \left(DIE\right)$$
9		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
10	6 1 9 7 8	catcisoi	$$⊢\phi \to \left(K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\wedge 1^{st}\left(K\right):B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_E\right)$$
11	10	simpld	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
12	1 2 3 4 5 11	uobffth	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 |-