Theorem uobeqw

Description: If a full functor (in fact, a full embedding) is a section of a fully faithful functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobeq.b	$$⊢B={\mathrm{Base}}_D$$
	uobeq.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
	uobeq.x	$$⊢\phi \to X\in B$$
	uobeq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobeq.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
	uobeq.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uobeq.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uobeq.n	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=I$$
	uobeqw.l	$$⊢\phi \to L\in \left(\left(E\mathrm{Full}D\right)\cap \left(E\mathrm{Faith}D\right)\right)$$
Assertion	uobeqw	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		uobeq.b	$$⊢B={\mathrm{Base}}_D$$
2		uobeq.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
3		uobeq.x	$$⊢\phi \to X\in B$$
4		uobeq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5		uobeq.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
6		uobeq.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
7		uobeq.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
8		uobeq.n	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=I$$
9		uobeqw.l	$$⊢\phi \to L\in \left(\left(E\mathrm{Full}D\right)\cap \left(E\mathrm{Faith}D\right)\right)$$
10		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 |-
11		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 |-
12	7	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 |-
13		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
14		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
15	14 5	sselid	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
16		1st2nd	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge K\in \left(D\mathrm{Func}E\right)\right)\to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
17	13 15 16	sylancr	$$⊢\phi \to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
18	15	func1st2nd	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Func}E\right)2^{nd}\left(K\right)$$
19		inss1	$$⊢\left(E\mathrm{Full}D\right)\cap \left(E\mathrm{Faith}D\right)\subseteq E\mathrm{Full}D$$
20		fullfunc	$$⊢E\mathrm{Full}D\subseteq E\mathrm{Func}D$$
21	19 20	sstri	$$⊢\left(E\mathrm{Full}D\right)\cap \left(E\mathrm{Faith}D\right)\subseteq E\mathrm{Func}D$$
22	21 9	sselid	$$⊢\phi \to L\in \left(E\mathrm{Func}D\right)$$
23	22	func1st2nd	$$⊢\phi \to 1^{st}\left(L\right)\left(E\mathrm{Func}D\right)2^{nd}\left(L\right)$$
24	15 22	cofu1st2nd	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=⟨1^{st}\left(L\right),2^{nd}\left(L\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
25	24 8	eqtr3d	$$⊢\phi \to ⟨1^{st}\left(L\right),2^{nd}\left(L\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩=I$$
26	2 18 23 25	cofidfth	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Faith}E\right)2^{nd}\left(K\right)$$
27		df-br	$$⊢1^{st}\left(K\right)\left(D\mathrm{Faith}E\right)2^{nd}\left(K\right)\leftrightarrow ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(D\mathrm{Faith}E\right)$$
28	26 27	sylib	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(D\mathrm{Faith}E\right)$$
29	17 28	eqeltrd	$$⊢\phi \to K\in \left(D\mathrm{Faith}E\right)$$
30	5 29	elind	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
31	30	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 |-
32	6	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 |-
33		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 |-
34		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 |-
35	12 31 32 33 34	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 |-
36		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 |-
37	11 35 36	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 |-
38	37	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 |-
39	10 38	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 |-
40		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 |-
41		fvexd	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) e. _V ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) e. _V ) with typecode |-
42	7	fveq2d	$$⊢\phi \to 1^{st}\left(L\right)\left(1^{st}\left(K\right)\left(X\right)\right)=1^{st}\left(L\right)\left(Y\right)$$
43	2 1 3 15 22 8	cofid1a	$$⊢\phi \to 1^{st}\left(L\right)\left(1^{st}\left(K\right)\left(X\right)\right)=X$$
44	42 43	eqtr3d	$$⊢\phi \to 1^{st}\left(L\right)\left(Y\right)=X$$
45	44	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` L ) ` Y ) = X ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( 1st ` L ) ` Y ) = X ) with typecode |-
46	9	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> L e. ( ( E Full D ) i^i ( E Faith D ) ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> L e. ( ( E Full D ) i^i ( E Faith D ) ) ) with typecode |-
47	4 15 22	cofuass	$$⊢\phi \to \left(L{\circ }_{\mathrm{func}}K\right){\circ }_{\mathrm{func}}F=L{\circ }_{\mathrm{func}}\left(K{\circ }_{\mathrm{func}}F\right)$$
48	8	oveq1d	$$⊢\phi \to \left(L{\circ }_{\mathrm{func}}K\right){\circ }_{\mathrm{func}}F=I{\circ }_{\mathrm{func}}F$$
49	4 2	cofulid	$$⊢\phi \to I{\circ }_{\mathrm{func}}F=F$$
50	48 49	eqtrd	$$⊢\phi \to \left(L{\circ }_{\mathrm{func}}K\right){\circ }_{\mathrm{func}}F=F$$
51	6	oveq2d	$$⊢\phi \to L{\circ }_{\mathrm{func}}\left(K{\circ }_{\mathrm{func}}F\right)=L{\circ }_{\mathrm{func}}G$$
52	47 50 51	3eqtr3rd	$$⊢\phi \to L{\circ }_{\mathrm{func}}G=F$$
53	52	adantr	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( L o.func G ) = F ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( L o.func G ) = F ) with typecode |-
54		eqidd	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) = ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) = ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) with typecode |-
55		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 |-
56	45 46 53 54 55	uptrai	Could not format ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) : No typesetting found for |- ( ( ph /\ z ( G ( C UP E ) Y ) n ) -> z ( F ( C UP D ) X ) ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) with typecode |-
57		breq2	Could not format ( m = ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) -> ( z ( F ( C UP D ) X ) m <-> z ( F ( C UP D ) X ) ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) ) : No typesetting found for |- ( m = ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) -> ( z ( F ( C UP D ) X ) m <-> z ( F ( C UP D ) X ) ( ( Y ( 2nd ` L ) ( ( 1st ` G ) ` z ) ) ` n ) ) ) with typecode |-
58	41 56 57	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 |-
59	58	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 |-
60	40 59	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 |-
61	39 60	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 |-
62		relup	Could not format Rel ( F ( C UP D ) X ) : No typesetting found for |- Rel ( F ( C UP D ) X ) with typecode |-
63		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 |-
64	62 63	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 |-
65		relup	Could not format Rel ( G ( C UP E ) Y ) : No typesetting found for |- Rel ( G ( C UP E ) Y ) with typecode |-
66		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 |-
67	65 66	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 |-
68	61 64 67	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 |-
69	68	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 |-