Theorem uobeqterm

Description: Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobeqterm.a	$$⊢A={\mathrm{Base}}_D$$
	uobeqterm.b	$$⊢B={\mathrm{Base}}_E$$
	uobeqterm.x	$$⊢\phi \to X\in A$$
	uobeqterm.y	$$⊢\phi \to Y\in B$$
	uobeqterm.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobeqterm.g	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
	uobeqterm.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
	uobeqterm.e	No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
Assertion	uobeqterm	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		uobeqterm.a	$$⊢A={\mathrm{Base}}_D$$
2		uobeqterm.b	$$⊢B={\mathrm{Base}}_E$$
3		uobeqterm.x	$$⊢\phi \to X\in A$$
4		uobeqterm.y	$$⊢\phi \to Y\in B$$
5		uobeqterm.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
6		uobeqterm.g	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
7		uobeqterm.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
8		uobeqterm.e	Could not format ( ph -> E e. TermCat ) : No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
9		eqid	$$⊢\mathrm{CatCat}\left(\left\{D,E\right\}\right)=\mathrm{CatCat}\left(\left\{D,E\right\}\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{CatCat}\left(\left\{D,E\right\}\right)}={\mathrm{Base}}_{\mathrm{CatCat}\left(\left\{D,E\right\}\right)}$$
11		prid1g	Could not format ( D e. TermCat -> D e. { D , E } ) : No typesetting found for |- ( D e. TermCat -> D e. { D , E } ) with typecode |-
12	7 11	syl	$$⊢\phi \to D\in \left\{D,E\right\}$$
13	7	termccatd	$$⊢\phi \to D\in \mathrm{Cat}$$
14	12 13	elind	$$⊢\phi \to D\in \left(\left\{D,E\right\}\cap \mathrm{Cat}\right)$$
15		prex	$$⊢\left\{D,E\right\}\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \left\{D,E\right\}\in \mathrm{V}$$
17	9 10 16	catcbas	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{CatCat}\left(\left\{D,E\right\}\right)}=\left\{D,E\right\}\cap \mathrm{Cat}$$
18	14 17	eleqtrrd	$$⊢\phi \to D\in {\mathrm{Base}}_{\mathrm{CatCat}\left(\left\{D,E\right\}\right)}$$
19		prid2g	Could not format ( E e. TermCat -> E e. { D , E } ) : No typesetting found for |- ( E e. TermCat -> E e. { D , E } ) with typecode |-
20	8 19	syl	$$⊢\phi \to E\in \left\{D,E\right\}$$
21	8	termccatd	$$⊢\phi \to E\in \mathrm{Cat}$$
22	20 21	elind	$$⊢\phi \to E\in \left(\left\{D,E\right\}\cap \mathrm{Cat}\right)$$
23	22 17	eleqtrrd	$$⊢\phi \to E\in {\mathrm{Base}}_{\mathrm{CatCat}\left(\left\{D,E\right\}\right)}$$
24	9 10 18 23 7	termcciso	Could not format ( ph -> ( E e. TermCat <-> D ( ~=c ` ( CatCat ` { D , E } ) ) E ) ) : No typesetting found for |- ( ph -> ( E e. TermCat <-> D ( ~=c ` ( CatCat ` { D , E } ) ) E ) ) with typecode |-
25	8 24	mpbid	$$⊢\phi \to D{\simeq }_{𝑐}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E$$
26		eqid	$$⊢\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)=\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)$$
27	9	catccat	$$⊢\left\{D,E\right\}\in \mathrm{V}\to \mathrm{CatCat}\left(\left\{D,E\right\}\right)\in \mathrm{Cat}$$
28	16 27	syl	$$⊢\phi \to \mathrm{CatCat}\left(\left\{D,E\right\}\right)\in \mathrm{Cat}$$
29	26 10 28 18 23	cic	$$⊢\phi \to \left(D{\simeq }_{𝑐}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\leftrightarrow \exists kk\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)$$
30	25 29	mpbid	$$⊢\phi \to \exists kk\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)$$
31	3	adantr	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to X\in A$$
32	5	adantr	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to F\in \left(C\mathrm{Func}D\right)$$
33		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
34		simpr	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)$$
35	9 1 2 26 34	catcisoi	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\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):A\underset{1-1\; onto}{⟶}B\right)$$
36	35	simpld	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to k\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
37	36	elin1d	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to k\in \left(D\mathrm{Full}E\right)$$
38	33 37	sselid	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to k\in \left(D\mathrm{Func}E\right)$$
39	6	adantr	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to G\in \left(C\mathrm{Func}E\right)$$
40	8	adantr	Could not format ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> E e. TermCat ) : No typesetting found for |- ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> E e. TermCat ) with typecode |-
41	32 38 39 40	cofuterm	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to k{\circ }_{\mathrm{func}}F=G$$
42	38	func1st2nd	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to 1^{st}\left(k\right)\left(D\mathrm{Func}E\right)2^{nd}\left(k\right)$$
43	1 2 42	funcf1	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to 1^{st}\left(k\right):A⟶B$$
44	43 31	ffvelcdmd	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to 1^{st}\left(k\right)\left(X\right)\in B$$
45	4	adantr	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to Y\in B$$
46	40 2 44 45	termcbasmo	$$⊢\left(\phi \wedge k\in \left(D\mathrm{Iso}\left(\mathrm{CatCat}\left(\left\{D,E\right\}\right)\right)E\right)\right)\to 1^{st}\left(k\right)\left(X\right)=Y$$
47	1 31 32 41 46 9 26 34	uobeq3	Could not format ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-
48	30 47	exlimddv	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 |-