uptr

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

	Ref	Expression
Hypotheses	uptr.y	$⊢ φ \to R (X) = Y$
	uptr.r	$⊢ φ \to R ((D Full E) \cap (D Faith E)) S$
	uptr.k	$⊢ φ \to ⟨R, S⟩ \circ_{func} ⟨F, G⟩ = ⟨K, L⟩$
	uptr.b	$⊢ B = {Base}_{D}$
	uptr.x	$⊢ φ \to X \in B$
	uptr.f	$⊢ φ \to F (C Func D) G$
	uptr.n	$⊢ φ \to (X S F (Z)) (M) = N$
	uptr.j	$⊢ J = Hom (D)$
	uptr.m	$⊢ φ \to M \in (X J F (Z))$
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	$⊢ φ \to R (X) = Y$
2		uptr.r	$⊢ φ \to R ((D Full E) \cap (D Faith E)) S$
3		uptr.k	$⊢ φ \to ⟨R, S⟩ \circ_{func} ⟨F, G⟩ = ⟨K, L⟩$
4		uptr.b	$⊢ B = {Base}_{D}$
5		uptr.x	$⊢ φ \to X \in B$
6		uptr.f	$⊢ φ \to F (C Func D) G$
7		uptr.n	$⊢ φ \to (X S F (Z)) (M) = N$
8		uptr.j	$⊢ J = Hom (D)$
9		uptr.m	$⊢ φ \to M \in (X J F (Z))$
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	$⊢ {Base}_{C} = {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 \|-

Metamath Proof Explorer

Theorem uptr

Proof