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	uobffth.b	$⊢ B = {Base}_{D}$
	uobffth.x	$⊢ φ \to X \in B$
	uobffth.f	$⊢ φ \to F \in (C Func D)$
	uobffth.g	$⊢ φ \to K \circ_{func} F = G$
	uobffth.y	$⊢ φ \to 1^{st} (K) (X) = Y$
	uobeq.i	$⊢ I = {id}_{func} (D)$
	uobeq.k	$⊢ φ \to K \in (D Full E)$
	uobeq.n	$⊢ φ \to L \circ_{func} K = I$
	uobeqw.l	$⊢ φ \to L \in ((E Full D) \cap (E Faith D))$
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		uobffth.b	$⊢ B = {Base}_{D}$
2		uobffth.x	$⊢ φ \to X \in B$
3		uobffth.f	$⊢ φ \to F \in (C Func D)$
4		uobffth.g	$⊢ φ \to K \circ_{func} F = G$
5		uobffth.y	$⊢ φ \to 1^{st} (K) (X) = Y$
6		uobeq.i	$⊢ I = {id}_{func} (D)$
7		uobeq.k	$⊢ φ \to K \in (D Full E)$
8		uobeq.n	$⊢ φ \to L \circ_{func} K = I$
9		uobeqw.l	$⊢ φ \to L \in ((E Full D) \cap (E Faith D))$
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	5	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	$⊢ Rel (D Func E)$
14		fullfunc	$⊢ D Full E \subseteq D Func E$
15	14 7	sselid	$⊢ φ \to K \in (D Func E)$
16		1st2nd	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
17	13 15 16	sylancr	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
18	15	func1st2nd	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
19		inss1	$⊢ (E Full D) \cap (E Faith D) \subseteq E Full D$
20		fullfunc	$⊢ E Full D \subseteq E Func D$
21	19 20	sstri	$⊢ (E Full D) \cap (E Faith D) \subseteq E Func D$
22	21 9	sselid	$⊢ φ \to L \in (E Func D)$
23	22	func1st2nd	$⊢ φ \to 1^{st} (L) (E Func D) 2^{nd} (L)$
24	15 22	cofu1st2nd	$⊢ φ \to L \circ_{func} K = ⟨1^{st} (L), 2^{nd} (L)⟩ \circ_{func} ⟨1^{st} (K), 2^{nd} (K)⟩$
25	24 8	eqtr3d	$⊢ φ \to ⟨1^{st} (L), 2^{nd} (L)⟩ \circ_{func} ⟨1^{st} (K), 2^{nd} (K)⟩ = I$
26	6 18 23 25	cofidfth	$⊢ φ \to 1^{st} (K) (D Faith E) 2^{nd} (K)$
27		df-br	$⊢ 1^{st} (K) (D Faith E) 2^{nd} (K) \leftrightarrow ⟨1^{st} (K), 2^{nd} (K)⟩ \in (D Faith E)$
28	26 27	sylib	$⊢ φ \to ⟨1^{st} (K), 2^{nd} (K)⟩ \in (D Faith E)$
29	17 28	eqeltrd	$⊢ φ \to K \in (D Faith E)$
30	7 29	elind	$⊢ φ \to K \in ((D Full E) \cap (D Faith E))$
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	4	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	5	fveq2d	$⊢ φ \to 1^{st} (L) (1^{st} (K) (X)) = 1^{st} (L) (Y)$
43	6 1 2 15 22 8	cofid1a	$⊢ φ \to 1^{st} (L) (1^{st} (K) (X)) = X$
44	42 43	eqtr3d	$⊢ φ \to 1^{st} (L) (Y) = 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	3 15 22	cofuass	$⊢ φ \to (L \circ_{func} K) \circ_{func} F = L \circ_{func} (K \circ_{func} F)$
48	8	oveq1d	$⊢ φ \to (L \circ_{func} K) \circ_{func} F = I \circ_{func} F$
49	3 6	cofulid	$⊢ φ \to I \circ_{func} F = F$
50	48 49	eqtrd	$⊢ φ \to (L \circ_{func} K) \circ_{func} F = F$
51	4	oveq2d	$⊢ φ \to L \circ_{func} (K \circ_{func} F) = L \circ_{func} G$
52	47 50 51	3eqtr3rd	$⊢ φ \to L \circ_{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 \|-

Metamath Proof Explorer

Theorem uobeqw

Proof