This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uptrai

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

		Ref	Expression
	Hypotheses	uptra.y	$⊢ φ \to 1^{st} (K) (X) = Y$
		uptra.k	$⊢ φ \to K \in ((D Full E) \cap (D Faith E))$
		uptra.g	$⊢ φ \to K \circ_{func} F = G$
		uptrai.n	$⊢ φ \to (X 2^{nd} (K) 1^{st} (F) (Z)) (M) = N$
		uptrai.z	No typesetting found for \|- ( ph -> Z ( F ( C UP D ) X ) M ) with typecode \|-
	Assertion	uptrai	Could not format assertion : No typesetting found for \|- ( ph -> Z ( G ( C UP E ) Y ) N ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		uptra.y	$⊢ φ \to 1^{st} (K) (X) = Y$
2		uptra.k	$⊢ φ \to K \in ((D Full E) \cap (D Faith E))$
3		uptra.g	$⊢ φ \to K \circ_{func} F = G$
4		uptrai.n	$⊢ φ \to (X 2^{nd} (K) 1^{st} (F) (Z)) (M) = N$
5		uptrai.z	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 \|-
6	1	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 \|-
7	2	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 \|-
8	3	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 \|-
9		eqid	$⊢ {Base}_{D} = {Base}_{D}$
10		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 \|-
11	10	up1st2nd	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M ) : No typesetting found for \|- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M ) with typecode \|-
12	11 9	uprcl3	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) : No typesetting found for \|- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) with typecode \|-
13	10	uprcl2a	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> F e. ( C Func D ) ) : No typesetting found for \|- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> F e. ( C Func D ) ) with typecode \|-
14	4	adantr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) : No typesetting found for \|- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) with typecode \|-
15		eqid	$⊢ Hom (D) = Hom (D)$
16	11 15	uprcl5	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) : No typesetting found for \|- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) with typecode \|-
17	6 7 8 9 12 13 14 15 16	uptra	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( 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 ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode \|-
18	5 17	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 \|-
19	5 18	mpbid	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 \|-