Theorem uptrar

Description: Universal property and fully faithful functor. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uptra.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uptra.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
	uptra.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uptra.b	$$⊢B={\mathrm{Base}}_D$$
	uptra.x	$$⊢\phi \to X\in B$$
	uptra.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uptrar.m	$$⊢\phi \to {\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)}^{-1}\left(N\right)=M$$
	uptrar.z	No typesetting found for |- ( ph -> Z ( G ( C UP E ) Y ) N ) with typecode |-
Assertion	uptrar	Could not format assertion : No typesetting found for |- ( ph -> Z ( F ( C UP D ) X ) M ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptra.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
2		uptra.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
3		uptra.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
4		uptra.b	$$⊢B={\mathrm{Base}}_D$$
5		uptra.x	$$⊢\phi \to X\in B$$
6		uptra.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
7		uptrar.m	$$⊢\phi \to {\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)}^{-1}\left(N\right)=M$$
8		uptrar.z	Could not format ( ph -> Z ( G ( C UP E ) Y ) N ) : No typesetting found for |- ( ph -> Z ( G ( C UP E ) Y ) N ) with typecode |-
9	1	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 |-
10	2	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 |-
11	3	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 |-
12	5	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 |-
13	6	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 |-
14	7	adantr	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) = M ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) = M ) with typecode |-
15	14	fveq2d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) ) with typecode |-
16		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
17		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
18		relfull	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)$$
19		relin1	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)\to \mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
20	18 19	ax-mp	$$⊢\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
21		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\wedge K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\right)\to 1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)$$
22	20 2 21	sylancr	$$⊢\phi \to 1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)$$
23	22	adantr	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) ) with typecode |-
24		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
25	13	func1st2nd	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) ) with typecode |-
26	24 4 25	funcf1	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) : ( Base ` C ) --> B ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) : ( Base ` C ) --> B ) 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	27	up1st2nd	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) with typecode |-
29	28 24	uprcl4	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) ) with typecode |-
30	26 29	ffvelcdmd	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` F ) ` Z ) e. B ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` F ) ` Z ) e. B ) with typecode |-
31	4 16 17 23 12 30	ffthf1o	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) ) with typecode |-
32		inss1	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Full}E$$
33		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
34	32 33	sstri	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Func}E$$
35	34 2	sselid	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
36	35	adantr	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> K e. ( D Func E ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> K e. ( D Func E ) ) with typecode |-
37	24 13 36 29	cofu1	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) with typecode |-
38	11	fveq2d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` ( K o.func F ) ) = ( 1st ` G ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` ( K o.func F ) ) = ( 1st ` G ) ) with typecode |-
39	38	fveq1d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` G ) ` Z ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` G ) ` Z ) ) with typecode |-
40	37 39	eqtr3d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) = ( ( 1st ` G ) ` Z ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) = ( ( 1st ` G ) ` Z ) ) with typecode |-
41	9 40	oveq12d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) = ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) = ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) with typecode |-
42	41	f1oeq3d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) <-> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) <-> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) ) with typecode |-
43	31 42	mpbid	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) with typecode |-
44	28 17	uprcl5	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> N e. ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> N e. ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) with typecode |-
45		f1ocnvfv2	$$⊢\left(\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right):X\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(Z\right)\underset{1-1\; onto}{⟶}Y\mathrm{Hom}\left(E\right)1^{st}\left(G\right)\left(Z\right)\wedge N\in \left(Y\mathrm{Hom}\left(E\right)1^{st}\left(G\right)\left(Z\right)\right)\right)\to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left({\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)}^{-1}\left(N\right)\right)=N$$
46	43 44 45	syl2anc	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = N ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = N ) with typecode |-
47	15 46	eqtr3d	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) with typecode |-
48		f1ocnvdm	$$⊢\left(\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right):X\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(Z\right)\underset{1-1\; onto}{⟶}Y\mathrm{Hom}\left(E\right)1^{st}\left(G\right)\left(Z\right)\wedge N\in \left(Y\mathrm{Hom}\left(E\right)1^{st}\left(G\right)\left(Z\right)\right)\right)\to {\left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)}^{-1}\left(N\right)\in \left(X\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(Z\right)\right)$$
49	43 44 48	syl2anc	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) with typecode |-
50	14 49	eqeltrrd	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) with typecode |-
51	9 10 11 4 12 13 47 16 50	uptra	Could not format ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode |-
52	8 51	mpdan	Could not format ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode |-
53	8 52	mpbird	Could not format ( ph -> Z ( F ( C UP D ) X ) M ) : No typesetting found for |- ( ph -> Z ( F ( C UP D ) X ) M ) with typecode |-