upfval2

Description: Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-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)$
	upfval2.w	$⊢ φ \to W \in C$
	upfval2.f	$⊢ φ \to F \in (D Func E)$
Assertion	upfval2	Could not format assertion : No typesetting found for \|- ( ph -> ( F ( D UP E ) W ) = { <. 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		upfval2.w	$⊢ φ \to W \in C$
7		upfval2.f	$⊢ φ \to F \in (D Func E)$
8		anass	$⊢ ((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))$
9	8	opabbii	$⊢ \{⟨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))\}$
10	1	fvexi	$⊢ B \in V$
11	10	a1i	$⊢ φ \to B \in V$
12		simprl	$⊢ ((φ \land 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)) \to m \in (W J 1^{st} (F) (x))$
13		ovexd	$⊢ (φ \land x \in B) \to W J 1^{st} (F) (x) \in V$
14	12 13	abexd	$⊢ (φ \land x \in B) \to \{m \| (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$
15	11 14	opabex3d	$⊢ φ \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))\} \in V$
16	9 15	eqeltrid	$⊢ φ \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)\} \in V$
17		fveq2	$⊢ f = F \to 1^{st} (f) = 1^{st} (F)$
18	17	fveq1d	$⊢ f = F \to 1^{st} (f) (x) = 1^{st} (F) (x)$
19	18	oveq2d	$⊢ f = F \to w J 1^{st} (f) (x) = w J 1^{st} (F) (x)$
20	19	eleq2d	$⊢ f = F \to (m \in (w J 1^{st} (f) (x)) \leftrightarrow m \in (w J 1^{st} (F) (x)))$
21	20	anbi2d	$⊢ f = F \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))))$
22	17	fveq1d	$⊢ f = F \to 1^{st} (f) (y) = 1^{st} (F) (y)$
23	22	oveq2d	$⊢ f = F \to w J 1^{st} (f) (y) = w J 1^{st} (F) (y)$
24	18	opeq2d	$⊢ f = F \to ⟨w, 1^{st} (f) (x)⟩ = ⟨w, 1^{st} (F) (x)⟩$
25	24 22	oveq12d	$⊢ f = F \to ⟨w, 1^{st} (f) (x)⟩ O 1^{st} (f) (y) = ⟨w, 1^{st} (F) (x)⟩ O 1^{st} (F) (y)$
26		fveq2	$⊢ f = F \to 2^{nd} (f) = 2^{nd} (F)$
27	26	oveqd	$⊢ f = F \to x 2^{nd} (f) y = x 2^{nd} (F) y$
28	27	fveq1d	$⊢ f = F \to (x 2^{nd} (f) y) (k) = (x 2^{nd} (F) y) (k)$
29		eqidd	$⊢ f = F \to m = m$
30	25 28 29	oveq123d	$⊢ f = F \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$
31	30	eqeq2d	$⊢ f = F \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)$
32	31	reubidv	$⊢ f = F \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)$
33	23 32	raleqbidv	$⊢ f = F \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)$
34	33	ralbidv	$⊢ f = F \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)$
35	21 34	anbi12d	$⊢ f = F \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))$
36	35	opabbidv	$⊢ f = F \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)\}$
37		oveq1	$⊢ w = W \to w J 1^{st} (F) (x) = W J 1^{st} (F) (x)$
38	37	eleq2d	$⊢ w = W \to (m \in (w J 1^{st} (F) (x)) \leftrightarrow m \in (W J 1^{st} (F) (x)))$
39	38	anbi2d	$⊢ w = W \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))))$
40		oveq1	$⊢ w = W \to w J 1^{st} (F) (y) = W J 1^{st} (F) (y)$
41		opeq1	$⊢ w = W \to ⟨w, 1^{st} (F) (x)⟩ = ⟨W, 1^{st} (F) (x)⟩$
42	41	oveq1d	$⊢ w = W \to ⟨w, 1^{st} (F) (x)⟩ O 1^{st} (F) (y) = ⟨W, 1^{st} (F) (x)⟩ O 1^{st} (F) (y)$
43	42	oveqd	$⊢ w = W \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$
44	43	eqeq2d	$⊢ w = W \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)$
45	44	reubidv	$⊢ w = W \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)$
46	40 45	raleqbidv	$⊢ w = W \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)$
47	46	ralbidv	$⊢ w = W \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)$
48	39 47	anbi12d	$⊢ w = W \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))$
49	48	opabbidv	$⊢ w = W \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)\}$
50	1 2 3 4 5	upfval	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 \|-
51	36 49 50	ovmpog	Could not format ( ( 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 ) ) } e. _V ) -> ( F ( D UP E ) W ) = { <. 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 \|- ( ( 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 ) ) } e. _V ) -> ( F ( D UP E ) W ) = { <. 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 \|-
52	7 6 16 51	syl3anc	Could not format ( ph -> ( F ( D UP E ) W ) = { <. 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 \|- ( ph -> ( F ( D UP E ) W ) = { <. 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 upfval2

Proof