upfval

Description: Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025) (Proof shortened by Zhi Wang, 12-Nov-2025)

	Ref	Expression
Hypotheses	upfval.b	$⊢ B = {Base}_{D}$
	upfval.c	$⊢ C = {Base}_{E}$
	upfval.h	$⊢ H = Hom (D)$
	upfval.j	$⊢ J = Hom (E)$
	upfval.o	$⊢ O = comp (E)$
Assertion	upfval	Could not format assertion : No typesetting found for \|- ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		upfval.b	$⊢ B = {Base}_{D}$
2		upfval.c	$⊢ C = {Base}_{E}$
3		upfval.h	$⊢ H = Hom (D)$
4		upfval.j	$⊢ J = Hom (E)$
5		upfval.o	$⊢ O = comp (E)$
6		fvexd	$⊢ (d = D \land e = E) \to {Base}_{d} \in V$
7		fveq2	$⊢ d = D \to {Base}_{d} = {Base}_{D}$
8	7	adantr	$⊢ (d = D \land e = E) \to {Base}_{d} = {Base}_{D}$
9	8 1	eqtr4di	$⊢ (d = D \land e = E) \to {Base}_{d} = B$
10		fvexd	$⊢ ((d = D \land e = E) \land b = B) \to {Base}_{e} \in V$
11		simplr	$⊢ ((d = D \land e = E) \land b = B) \to e = E$
12	11	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to {Base}_{e} = {Base}_{E}$
13	12 2	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to {Base}_{e} = C$
14		fvexd	$⊢ (((d = D \land e = E) \land b = B) \land c = C) \to Hom (d) \in V$
15		simplll	$⊢ (((d = D \land e = E) \land b = B) \land c = C) \to d = D$
16	15	fveq2d	$⊢ (((d = D \land e = E) \land b = B) \land c = C) \to Hom (d) = Hom (D)$
17	16 3	eqtr4di	$⊢ (((d = D \land e = E) \land b = B) \land c = C) \to Hom (d) = H$
18		fvexd	$⊢ ((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \to Hom (e) \in V$
19		simp-4r	$⊢ ((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \to e = E$
20	19	fveq2d	$⊢ ((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \to Hom (e) = Hom (E)$
21	20 4	eqtr4di	$⊢ ((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \to Hom (e) = J$
22		fvexd	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to comp (e) \in V$
23		simp-5r	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to e = E$
24	23	fveq2d	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to comp (e) = comp (E)$
25	24 5	eqtr4di	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to comp (e) = O$
26		simp-6l	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to d = D$
27		simp-6r	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to e = E$
28	26 27	oveq12d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to d Func e = D Func E$
29		simp-4r	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to c = C$
30		simp-5r	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to b = B$
31	30	eleq2d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (x \in b \leftrightarrow x \in B)$
32		simplr	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to j = J$
33	32	oveqd	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to w j 1^{st} (f) (x) = w J 1^{st} (f) (x)$
34	33	eleq2d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (m \in (w j 1^{st} (f) (x)) \leftrightarrow m \in (w J 1^{st} (f) (x)))$
35	31 34	anbi12d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to ((x \in b \land m \in (w j 1^{st} (f) (x))) \leftrightarrow (x \in B \land m \in (w J 1^{st} (f) (x))))$
36	32	oveqd	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to w j 1^{st} (f) (y) = w J 1^{st} (f) (y)$
37		simplr	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to h = H$
38	37	oveqdr	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to x h y = x H y$
39		simpr	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to o = O$
40	39	oveqd	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to ⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y) = ⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)$
41	40	oveqd	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m$
42	41	eqeq2d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m \leftrightarrow g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)$
43	38 42	reueqbidv	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (\exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m \leftrightarrow \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)$
44	36 43	raleqbidv	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (\forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m \leftrightarrow \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)$
45	30 44	raleqbidv	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (\forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m \leftrightarrow \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)$
46	35 45	anbi12d	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m) \leftrightarrow ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m))$
47	46	opabbidv	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\} = \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\}$
48	28 29 47	mpoeq123dv	$⊢ ((((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \land o = O) \to (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
49	22 25 48	csbied2	$⊢ (((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \land j = J) \to ⦋ comp (e) / o ⦌ (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
50	18 21 49	csbied2	$⊢ ((((d = D \land e = E) \land b = B) \land c = C) \land h = H) \to ⦋ Hom (e) / j ⦌ ⦋ comp (e) / o ⦌ (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
51	14 17 50	csbied2	$⊢ (((d = D \land e = E) \land b = B) \land c = C) \to ⦋ Hom (d) / h ⦌ ⦋ Hom (e) / j ⦌ ⦋ comp (e) / o ⦌ (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
52	10 13 51	csbied2	$⊢ ((d = D \land e = E) \land b = B) \to ⦋ {Base}_{e} / c ⦌ ⦋ Hom (d) / h ⦌ ⦋ Hom (e) / j ⦌ ⦋ comp (e) / o ⦌ (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
53	6 9 52	csbied2	$⊢ (d = D \land e = E) \to ⦋ {Base}_{d} / b ⦌ ⦋ {Base}_{e} / c ⦌ ⦋ Hom (d) / h ⦌ ⦋ Hom (e) / j ⦌ ⦋ comp (e) / o ⦌ (f \in (d Func e), w \in c ⟼ \{⟨x, m⟩ \| ((x \in b \land m \in (w j 1^{st} (f) (x))) \land \forall y \in b \forall g \in (w j 1^{st} (f) (y)) \exists! k \in (x h y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ o 1^{st} (f) (y)) m)\}) = (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\})$
54		df-up	Could not format UP = ( d e. _V , e e. _V \|-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c \|-> { <. x , m >. \| ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) ) : No typesetting found for \|- UP = ( d e. _V , e e. _V \|-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c \|-> { <. x , m >. \| ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) ) with typecode \|-
55		ovex	$⊢ D Func E \in V$
56	2	fvexi	$⊢ C \in V$
57	55 56	mpoex	$⊢ (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\}) \in V$
58	53 54 57	ovmpoa	Could not format ( ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) ) : No typesetting found for \|- ( ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) ) with typecode \|-
59		reldmup	Could not format Rel dom UP : No typesetting found for \|- Rel dom UP with typecode \|-
60	59	ovprc	Could not format ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = (/) ) : No typesetting found for \|- ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = (/) ) with typecode \|-
61		reldmfunc	$⊢ Rel dom Func$
62	61	ovprc	$⊢ \neg (D \in V \land E \in V) \to D Func E = \emptyset$
63	62	orcd	$⊢ \neg (D \in V \land E \in V) \to (D Func E = \emptyset \lor C = \emptyset)$
64		0mpo0	$⊢ (D Func E = \emptyset \lor C = \emptyset) \to (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\}) = \emptyset$
65	63 64	syl	$⊢ \neg (D \in V \land E \in V) \to (f \in (D Func E), w \in C ⟼ \{⟨x, m⟩ \| ((x \in B \land m \in (w J 1^{st} (f) (x))) \land \forall y \in B \forall g \in (w J 1^{st} (f) (y)) \exists! k \in (x H y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y)) m)\}) = \emptyset$
66	60 65	eqtr4d	Could not format ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) ) : No typesetting found for \|- ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) ) with typecode \|-
67	58 66	pm2.61i	Could not format ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) : No typesetting found for \|- ( D UP E ) = ( f e. ( D Func E ) , w e. C \|-> { <. x , m >. \| ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) with typecode \|-

Metamath Proof Explorer

Theorem upfval

Proof