Theorem uobeq

Description: If a full functor (in fact, a full embedding) is a section of a 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$$
	uobeq.l	$$⊢\phi \to L\in \left(E\mathrm{Func}D\right)$$
Assertion	uobeq	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		uobeq.l	$$⊢\phi \to L\in \left(E\mathrm{Func}D\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	9	func1st2nd	$$⊢\phi \to 1^{st}\left(L\right)\left(E\mathrm{Func}D\right)2^{nd}\left(L\right)$$
20	15 9	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)⟩$$
21	20 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$$
22	2 18 19 21	cofidfth	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Faith}E\right)2^{nd}\left(K\right)$$
23		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)$$
24	22 23	sylib	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(D\mathrm{Faith}E\right)$$
25	17 24	eqeltrd	$$⊢\phi \to K\in \left(D\mathrm{Faith}E\right)$$
26	5 25	elind	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
27	26	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 |-
28	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 |-
29		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 |-
30		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 |-
31	12 27 28 29 30	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 |-
32		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 |-
33	11 31 32	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 |-
34	33	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 |-
35	10 34	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 |-
36		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 |-
37		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 |-
38	7	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 |-
39	26	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 |-
40	6	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 |-
41	3	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 |-
42	4	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 |-
43		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 |-
44		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 |-
45	38 39 40 1 41 42 43 44	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 |-
46		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 |-
47	37 45 46	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 |-
48	47	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 |-
49	36 48	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 |-
50	35 49	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 |-
51		relup	Could not format Rel ( F ( C UP D ) X ) : No typesetting found for |- Rel ( F ( C UP D ) X ) with typecode |-
52		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 |-
53	51 52	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 |-
54		relup	Could not format Rel ( G ( C UP E ) Y ) : No typesetting found for |- Rel ( G ( C UP E ) Y ) with typecode |-
55		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 |-
56	54 55	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 |-
57	50 53 56	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 |-
58	57	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 |-