ixpovf

Description: A member of an indexed product of function spaces has the indicated function type at each pair of indices. Hom-functions of a functor are one application. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	ixpovf.p	⊢ ( 𝜑 → 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) )
	ixpovf.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	ixpovf.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
Assertion	ixpovf	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) : ( 𝑈 𝐻 𝑉 ) ⟶ ( ( 𝑂 ‘ 𝑈 ) 𝑁 ( 𝑂 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ixpovf.p	⊢ ( 𝜑 → 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) )
2		ixpovf.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
3		ixpovf.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
4	2 3	opelxpd	⊢ ( 𝜑 → ⟨ 𝑈 , 𝑉 ⟩ ∈ ( 𝑊 × 𝑊 ) )
5		2fveq3	⊢ ( 𝑧 = ⟨ 𝑈 , 𝑉 ⟩ → ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) = ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) )
6		2fveq3	⊢ ( 𝑧 = ⟨ 𝑈 , 𝑉 ⟩ → ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) = ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) )
7	5 6	oveq12d	⊢ ( 𝑧 = ⟨ 𝑈 , 𝑉 ⟩ → ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) )
8		fveq2	⊢ ( 𝑧 = ⟨ 𝑈 , 𝑉 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) )
9	7 8	oveq12d	⊢ ( 𝑧 = ⟨ 𝑈 , 𝑉 ⟩ → ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) = ( ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) ↑_m ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) )
10	9	fvixp	⊢ ( ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ⟨ 𝑈 , 𝑉 ⟩ ∈ ( 𝑊 × 𝑊 ) ) → ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ∈ ( ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) ↑_m ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) )
11	1 4 10	syl2anc	⊢ ( 𝜑 → ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ∈ ( ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) ↑_m ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) )
12	11	elmaprd	⊢ ( 𝜑 → ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) : ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ⟶ ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) )
13		df-ov	⊢ ( 𝑈 𝑃 𝑉 ) = ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ )
14	13	eqcomi	⊢ ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = ( 𝑈 𝑃 𝑉 )
15	14	a1i	⊢ ( 𝜑 → ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = ( 𝑈 𝑃 𝑉 ) )
16		df-ov	⊢ ( 𝑈 𝐻 𝑉 ) = ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ )
17	16	eqcomi	⊢ ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = ( 𝑈 𝐻 𝑉 )
18	17	a1i	⊢ ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = ( 𝑈 𝐻 𝑉 ) )
19	2	elexd	⊢ ( 𝜑 → 𝑈 ∈ V )
20	3	elexd	⊢ ( 𝜑 → 𝑉 ∈ V )
21		op1stg	⊢ ( ( 𝑈 ∈ V ∧ 𝑉 ∈ V ) → ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = 𝑈 )
22	19 20 21	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = 𝑈 )
23	22	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) = ( 𝑂 ‘ 𝑈 ) )
24		op2ndg	⊢ ( ( 𝑈 ∈ V ∧ 𝑉 ∈ V ) → ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = 𝑉 )
25	19 20 24	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) = 𝑉 )
26	25	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) = ( 𝑂 ‘ 𝑉 ) )
27	23 26	oveq12d	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) = ( ( 𝑂 ‘ 𝑈 ) 𝑁 ( 𝑂 ‘ 𝑉 ) ) )
28	15 18 27	feq123d	⊢ ( 𝜑 → ( ( 𝑃 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) : ( 𝐻 ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ⟶ ( ( 𝑂 ‘ ( 1^st ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) 𝑁 ( 𝑂 ‘ ( 2^nd ‘ ⟨ 𝑈 , 𝑉 ⟩ ) ) ) ↔ ( 𝑈 𝑃 𝑉 ) : ( 𝑈 𝐻 𝑉 ) ⟶ ( ( 𝑂 ‘ 𝑈 ) 𝑁 ( 𝑂 ‘ 𝑉 ) ) ) )
29	12 28	mpbid	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) : ( 𝑈 𝐻 𝑉 ) ⟶ ( ( 𝑂 ‘ 𝑈 ) 𝑁 ( 𝑂 ‘ 𝑉 ) ) )

Metamath Proof Explorer

Theorem ixpovf

Proof