uptrar

Description: Universal property and fully faithful functor. (Contributed by Zhi Wang, 17-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)$
	uptrar.m	$⊢ φ \to {(X 2^{nd} (K) 1^{st} (F) (Z))}^{-1} (N) = 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	$⊢ φ \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		uptrar.m	$⊢ φ \to {(X 2^{nd} (K) 1^{st} (F) (Z))}^{-1} (N) = 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	$⊢ Hom (D) = Hom (D)$
17		eqid	$⊢ Hom (E) = Hom (E)$
18		relfull	$⊢ Rel (D Full E)$
19		relin1	$⊢ Rel (D Full E) \to Rel ((D Full E) \cap (D Faith E))$
20	18 19	ax-mp	$⊢ Rel ((D Full E) \cap (D Faith E))$
21		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)$
22	20 2 21	sylancr	$⊢ φ \to 1^{st} (K) ((D Full E) \cap (D Faith E)) 2^{nd} (K)$
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	$⊢ {Base}_{C} = {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	$⊢ (D Full E) \cap (D Faith E) \subseteq D Full E$
33		fullfunc	$⊢ D Full E \subseteq D Func E$
34	32 33	sstri	$⊢ (D Full E) \cap (D Faith E) \subseteq D Func E$
35	34 2	sselid	$⊢ φ \to K \in (D Func E)$
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	$⊢ ((X 2^{nd} (K) 1^{st} (F) (Z)) : X Hom (D) 1^{st} (F) (Z) \underset{1-1 onto}{⟶} Y Hom (E) 1^{st} (G) (Z) \land N \in (Y Hom (E) 1^{st} (G) (Z))) \to (X 2^{nd} (K) 1^{st} (F) (Z)) ({(X 2^{nd} (K) 1^{st} (F) (Z))}^{-1} (N)) = 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	$⊢ ((X 2^{nd} (K) 1^{st} (F) (Z)) : X Hom (D) 1^{st} (F) (Z) \underset{1-1 onto}{⟶} Y Hom (E) 1^{st} (G) (Z) \land N \in (Y Hom (E) 1^{st} (G) (Z))) \to {(X 2^{nd} (K) 1^{st} (F) (Z))}^{-1} (N) \in (X Hom (D) 1^{st} (F) (Z))$
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 \|-

Metamath Proof Explorer

Theorem uptrar

Proof