Theorem uptr

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

	Ref	Expression
Hypotheses	uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
	uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
	uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
	uptr.b	$$⊢B={\mathrm{Base}}_D$$
	uptr.x	$$⊢\phi \to X\in B$$
	uptr.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	uptr.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
	uptr.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	uptr.m	$$⊢\phi \to M\in \left(XJF\left(Z\right)\right)$$
Assertion	uptr	Could not format assertion : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
2		uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
3		uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
4		uptr.b	$$⊢B={\mathrm{Base}}_D$$
5		uptr.x	$$⊢\phi \to X\in B$$
6		uptr.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
7		uptr.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
8		uptr.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
9		uptr.m	$$⊢\phi \to M\in \left(XJF\left(Z\right)\right)$$
10		simpr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M ) with typecode |-
11		simpr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. K , L >. ( C UP E ) Y ) N ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. K , L >. ( C UP E ) Y ) N ) with typecode |-
12	1	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( R ` X ) = Y ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( R ` X ) = Y ) with typecode |-
13	2	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) with typecode |-
14	3	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) with typecode |-
15	5	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> X e. B ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> X e. B ) with typecode |-
16	6	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> F ( C Func D ) G ) with typecode |-
17	7	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) with typecode |-
18	9	adantr	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> M e. ( X J ( F ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> M e. ( X J ( F ` Z ) ) ) with typecode |-
19		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
20	11 19	uprcl4	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) ) with typecode |-
21	12 13 14 4 15 16 17 8 18 19 20	uptrlem3	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-
22	11 21	mpbird	Could not format ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. F , G >. ( C UP D ) X ) M ) : No typesetting found for |- ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. F , G >. ( C UP D ) X ) M ) with typecode |-
23	1	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y ) with typecode |-
24	2	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) with typecode |-
25	3	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) with typecode |-
26	5	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. B ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. B ) with typecode |-
27	6	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G ) with typecode |-
28	7	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) with typecode |-
29	9	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X J ( F ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X J ( F ` Z ) ) ) with typecode |-
30	10 19	uprcl4	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z e. ( Base ` C ) ) with typecode |-
31	23 24 25 4 26 27 28 8 29 19 30	uptrlem3	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-
32	10 22 31	bibiad	Could not format ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-