uptra

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$
	uptra.b	$⊢ B = {Base}_{D}$
	uptra.x	$⊢ φ \to X \in B$
	uptra.f	$⊢ φ \to F \in (C Func D)$
	uptra.n	$⊢ φ \to (X 2^{nd} (K) 1^{st} (F) (Z)) (M) = N$
	uptra.j	$⊢ J = Hom (D)$
	uptra.m	$⊢ φ \to M \in (X J 1^{st} (F) (Z))$
Assertion	uptra	Could not format assertion : No typesetting found for \|- ( ph -> ( Z ( F ( C UP D ) X ) M <-> 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		uptra.b	$⊢ B = {Base}_{D}$
5		uptra.x	$⊢ φ \to X \in B$
6		uptra.f	$⊢ φ \to F \in (C Func D)$
7		uptra.n	$⊢ φ \to (X 2^{nd} (K) 1^{st} (F) (Z)) (M) = N$
8		uptra.j	$⊢ J = Hom (D)$
9		uptra.m	$⊢ φ \to M \in (X J 1^{st} (F) (Z))$
10		relfull	$⊢ Rel (D Full E)$
11		relin1	$⊢ Rel (D Full E) \to Rel ((D Full E) \cap (D Faith E))$
12	10 11	ax-mp	$⊢ Rel ((D Full E) \cap (D Faith E))$
13		1st2ndbr	$⊢ (Rel ((D Full E) \cap (D Faith E)) \land K \in ((D Full E) \cap (D Faith E))) \to 1^{st} (K) ((D Full E) \cap (D Faith E)) 2^{nd} (K)$
14	12 2 13	sylancr	$⊢ φ \to 1^{st} (K) ((D Full E) \cap (D Faith E)) 2^{nd} (K)$
15		inss1	$⊢ (D Full E) \cap (D Faith E) \subseteq D Full E$
16		fullfunc	$⊢ D Full E \subseteq D Func E$
17	15 16	sstri	$⊢ (D Full E) \cap (D Faith E) \subseteq D Func E$
18	17 2	sselid	$⊢ φ \to K \in (D Func E)$
19	6 18	cofu1st2nd	$⊢ φ \to K \circ_{func} F = ⟨1^{st} (K), 2^{nd} (K)⟩ \circ_{func} ⟨1^{st} (F), 2^{nd} (F)⟩$
20		relfunc	$⊢ Rel (C Func E)$
21	6 18	cofucl	$⊢ φ \to K \circ_{func} F \in (C Func E)$
22	3 21	eqeltrrd	$⊢ φ \to G \in (C Func E)$
23		1st2nd	$⊢ (Rel (C Func E) \land G \in (C Func E)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
24	20 22 23	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
25	3 19 24	3eqtr3d	$⊢ φ \to ⟨1^{st} (K), 2^{nd} (K)⟩ \circ_{func} ⟨1^{st} (F), 2^{nd} (F)⟩ = ⟨1^{st} (G), 2^{nd} (G)⟩$
26	6	func1st2nd	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
27	1 14 25 4 5 26 7 8 9	uptr	Could not format ( ph -> ( Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) : No typesetting found for \|- ( ph -> ( Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) with typecode \|-
28	6	up1st2ndb	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 \|-
29	22	up1st2ndb	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 \|-
30	27 28 29	3bitr4d	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 \|-

Metamath Proof Explorer

Theorem uptra

Proof