upfval3

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

	Ref	Expression
Hypotheses	upfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	upfval.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	upfval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	upfval.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	upfval.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
	upfval2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
	upfval3.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
Assertion	upfval3	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		upfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		upfval.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
3		upfval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		upfval.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
5		upfval.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
6		upfval2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
7		upfval3.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
8		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
9	7 8	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
10	1 2 3 4 5 6 9	upfval2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ) } )
11		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
12	11	brrelex12i	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
13		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
14	12 13	syl	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
15	14	fveq1d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
16	15	oveq2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) = ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) )
17	16	eleq2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ↔ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) )
18	17	anbi2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ) )
19	14	fveq1d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
20	19	oveq2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) = ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
21	15	opeq2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ = ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ )
22	21 19	oveq12d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) = ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
23		op2ndg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
24	12 23	syl	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
25	24	oveqd	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
26	25	fveq1d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) = ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) )
27		eqidd	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝑚 = 𝑚 )
28	22 26 27	oveq123d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) )
29	28	eqeq2d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ↔ 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) )
30	29	reubidv	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) )
31	20 30	raleqbidv	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) )
32	31	ralbidv	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) )
33	18 32	anbi12d	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) ) )
34	33	opabbidv	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) } )
35	7 34	syl	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) } )
36	10 35	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑥 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑚 ) ) } )

Metamath Proof Explorer

Theorem upfval3

Proof