upfval2

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	⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
	upfval2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	upfval2	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } )

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		upfval2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
8		anass	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
9	8	opabbii	⊢ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) }
10	1	fvexi	⊢ 𝐵 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
12		simprl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) → 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
13		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ V )
14	12 13	abexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → { 𝑚 ∣ ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } ∈ V )
15	11 14	opabex3d	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ ( 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) } ∈ V )
16	9 15	eqeltrid	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } ∈ V )
17		fveq2	⊢ ( 𝑓 = 𝐹 → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
18	17	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) )
19	18	oveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
20	19	eleq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ↔ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
21	20	anbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
22	17	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
23	22	oveq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
24	18	opeq2d	⊢ ( 𝑓 = 𝐹 → ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ )
25	24 22	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
26		fveq2	⊢ ( 𝑓 = 𝐹 → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
27	26	oveqd	⊢ ( 𝑓 = 𝐹 → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
28	27	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) )
29		eqidd	⊢ ( 𝑓 = 𝐹 → 𝑚 = 𝑚 )
30	25 28 29	oveq123d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) )
31	30	eqeq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
32	31	reubidv	⊢ ( 𝑓 = 𝐹 → ( ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
33	23 32	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
34	33	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
35	21 34	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
36	35	opabbidv	⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
37		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
38	37	eleq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ↔ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
39	38	anbi2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
40		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
41		opeq1	⊢ ( 𝑤 = 𝑊 → ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ )
42	41	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
43	42	oveqd	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) )
44	43	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ↔ 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
45	44	reubidv	⊢ ( 𝑤 = 𝑊 → ( ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
46	40 45	raleqbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
47	46	ralbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) )
48	39 47	anbi12d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
49	48	opabbidv	⊢ ( 𝑤 = 𝑊 → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
50	1 2 3 4 5	upfval	⊢ ( 𝐷 UP 𝐸 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑤 ∈ 𝐶 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑤 𝐽 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
51	36 49 50	ovmpog	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑊 ∈ 𝐶 ∧ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } ∈ V ) → ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
52	7 6 16 51	syl3anc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑚 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 𝐻 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ 𝑂 ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) 𝑚 ) ) } )

Metamath Proof Explorer

Theorem upfval2

Proof