uobffth

Description: A fully faithful functor generates equal sets of universal objects. (Contributed by Zhi Wang, 19-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$
	uobffth.k	$⊢ φ \to K \in ((D Full E) \cap (D Faith E))$
Assertion	uobffth	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		uobffth.k	$⊢ φ \to K \in ((D Full E) \cap (D Faith E))$
7		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 \|-
8		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 \|-
9	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 \|-
10	6	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 \|-
11	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 \|-
12		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 \|-
13		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 \|-
14	9 10 11 12 13	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 \|-
15		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 \|-
16	8 14 15	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 \|-
17	16	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 \|-
18	7 17	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 \|-
19		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 \|-
20		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 \|-
21	5	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 \|-
22	6	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 \|-
23	4	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 \|-
24	2	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 \|-
25	3	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 \|-
26		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 \|-
27		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 \|-
28	21 22 23 1 24 25 26 27	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 \|-
29		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 \|-
30	20 28 29	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 \|-
31	30	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 \|-
32	19 31	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 \|-
33	18 32	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 \|-
34		relup	Could not format Rel ( F ( C UP D ) X ) : No typesetting found for \|- Rel ( F ( C UP D ) X ) with typecode \|-
35		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 \|-
36	34 35	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 \|-
37		relup	Could not format Rel ( G ( C UP E ) Y ) : No typesetting found for \|- Rel ( G ( C UP E ) Y ) with typecode \|-
38		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 \|-
39	37 38	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 \|-
40	33 36 39	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 \|-
41	40	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 uobffth

Proof