upfval3

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$
	upfval3.f	$⊢ φ \to F (D Func E) G$
Assertion	upfval3	Could not format assertion : No typesetting found for \|- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( 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		upfval3.f	$⊢ φ \to F (D Func E) G$
8		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
9	7 8	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
10	1 2 3 4 5 6 9	upfval2	Could not format ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) } ) : No typesetting found for \|- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( ( 1st ` <. F , G >. ) ` x ) ) ) /\ A. y e. B A. g e. ( W J ( ( 1st ` <. F , G >. ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` <. F , G >. ) y ) ` k ) ( <. W , ( ( 1st ` <. F , G >. ) ` x ) >. O ( ( 1st ` <. F , G >. ) ` y ) ) m ) ) } ) with typecode \|-
11		relfunc	$⊢ Rel (D Func E)$
12	11	brrelex12i	$⊢ F (D Func E) G \to (F \in V \land G \in V)$
13		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
14	12 13	syl	$⊢ F (D Func E) G \to 1^{st} (⟨F, G⟩) = F$
15	14	fveq1d	$⊢ F (D Func E) G \to 1^{st} (⟨F, G⟩) (x) = F (x)$
16	15	oveq2d	$⊢ F (D Func E) G \to W J 1^{st} (⟨F, G⟩) (x) = W J F (x)$
17	16	eleq2d	$⊢ F (D Func E) G \to (m \in (W J 1^{st} (⟨F, G⟩) (x)) \leftrightarrow m \in (W J F (x)))$
18	17	anbi2d	$⊢ F (D Func E) G \to ((x \in B \land m \in (W J 1^{st} (⟨F, G⟩) (x))) \leftrightarrow (x \in B \land m \in (W J F (x))))$
19	14	fveq1d	$⊢ F (D Func E) G \to 1^{st} (⟨F, G⟩) (y) = F (y)$
20	19	oveq2d	$⊢ F (D Func E) G \to W J 1^{st} (⟨F, G⟩) (y) = W J F (y)$
21	15	opeq2d	$⊢ F (D Func E) G \to ⟨W, 1^{st} (⟨F, G⟩) (x)⟩ = ⟨W, F (x)⟩$
22	21 19	oveq12d	$⊢ F (D Func E) G \to ⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y) = ⟨W, F (x)⟩ O F (y)$
23		op2ndg	$⊢ (F \in V \land G \in V) \to 2^{nd} (⟨F, G⟩) = G$
24	12 23	syl	$⊢ F (D Func E) G \to 2^{nd} (⟨F, G⟩) = G$
25	24	oveqd	$⊢ F (D Func E) G \to x 2^{nd} (⟨F, G⟩) y = x G y$
26	25	fveq1d	$⊢ F (D Func E) G \to (x 2^{nd} (⟨F, G⟩) y) (k) = (x G y) (k)$
27		eqidd	$⊢ F (D Func E) G \to m = m$
28	22 26 27	oveq123d	$⊢ F (D Func E) G \to (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m$
29	28	eqeq2d	$⊢ F (D Func E) G \to (g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m \leftrightarrow g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)$
30	29	reubidv	$⊢ F (D Func E) G \to (\exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m \leftrightarrow \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)$
31	20 30	raleqbidv	$⊢ F (D Func E) G \to (\forall g \in (W J 1^{st} (⟨F, G⟩) (y)) \exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m \leftrightarrow \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)$
32	31	ralbidv	$⊢ F (D Func E) G \to (\forall y \in B \forall g \in (W J 1^{st} (⟨F, G⟩) (y)) \exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m \leftrightarrow \forall y \in B \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)$
33	18 32	anbi12d	$⊢ F (D Func E) G \to (((x \in B \land m \in (W J 1^{st} (⟨F, G⟩) (x))) \land \forall y \in B \forall g \in (W J 1^{st} (⟨F, G⟩) (y)) \exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m) \leftrightarrow ((x \in B \land m \in (W J F (x))) \land \forall y \in B \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m))$
34	33	opabbidv	$⊢ F (D Func E) G \to \{⟨x, m⟩ \| ((x \in B \land m \in (W J 1^{st} (⟨F, G⟩) (x))) \land \forall y \in B \forall g \in (W J 1^{st} (⟨F, G⟩) (y)) \exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m)\} = \{⟨x, m⟩ \| ((x \in B \land m \in (W J F (x))) \land \forall y \in B \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)\}$
35	7 34	syl	$⊢ φ \to \{⟨x, m⟩ \| ((x \in B \land m \in (W J 1^{st} (⟨F, G⟩) (x))) \land \forall y \in B \forall g \in (W J 1^{st} (⟨F, G⟩) (y)) \exists! k \in (x H y) g = (x 2^{nd} (⟨F, G⟩) y) (k) (⟨W, 1^{st} (⟨F, G⟩) (x)⟩ O 1^{st} (⟨F, G⟩) (y)) m)\} = \{⟨x, m⟩ \| ((x \in B \land m \in (W J F (x))) \land \forall y \in B \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m)\}$
36	10 35	eqtrd	Could not format ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) : No typesetting found for \|- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) with typecode \|-

Metamath Proof Explorer

Theorem upfval3

Proof