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	$⊢ φ \to P \in \underset{z \in W \times W}{⨉} ({(O (1^{st} (z)) N O (2^{nd} (z)))}^{H (z)})$
	ixpovf.u	$⊢ φ \to U \in W$
	ixpovf.v	$⊢ φ \to V \in W$
Assertion	ixpovf	$⊢ φ \to (U P V) : U H V ⟶ O (U) N O (V)$

Proof

Step	Hyp	Ref	Expression
1		ixpovf.p	$⊢ φ \to P \in \underset{z \in W \times W}{⨉} ({(O (1^{st} (z)) N O (2^{nd} (z)))}^{H (z)})$
2		ixpovf.u	$⊢ φ \to U \in W$
3		ixpovf.v	$⊢ φ \to V \in W$
4	2 3	opelxpd	$⊢ φ \to ⟨U, V⟩ \in (W \times W)$
5		2fveq3	$⊢ z = ⟨U, V⟩ \to O (1^{st} (z)) = O (1^{st} (⟨U, V⟩))$
6		2fveq3	$⊢ z = ⟨U, V⟩ \to O (2^{nd} (z)) = O (2^{nd} (⟨U, V⟩))$
7	5 6	oveq12d	$⊢ z = ⟨U, V⟩ \to O (1^{st} (z)) N O (2^{nd} (z)) = O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩))$
8		fveq2	$⊢ z = ⟨U, V⟩ \to H (z) = H (⟨U, V⟩)$
9	7 8	oveq12d	$⊢ z = ⟨U, V⟩ \to {(O (1^{st} (z)) N O (2^{nd} (z)))}^{H (z)} = {(O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩)))}^{H (⟨U, V⟩)}$
10	9	fvixp	$⊢ (P \in \underset{z \in W \times W}{⨉} ({(O (1^{st} (z)) N O (2^{nd} (z)))}^{H (z)}) \land ⟨U, V⟩ \in (W \times W)) \to P (⟨U, V⟩) \in ({(O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩)))}^{H (⟨U, V⟩)})$
11	1 4 10	syl2anc	$⊢ φ \to P (⟨U, V⟩) \in ({(O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩)))}^{H (⟨U, V⟩)})$
12	11	elmaprd	$⊢ φ \to P (⟨U, V⟩) : H (⟨U, V⟩) ⟶ O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩))$
13		df-ov	$⊢ U P V = P (⟨U, V⟩)$
14	13	eqcomi	$⊢ P (⟨U, V⟩) = U P V$
15	14	a1i	$⊢ φ \to P (⟨U, V⟩) = U P V$
16		df-ov	$⊢ U H V = H (⟨U, V⟩)$
17	16	eqcomi	$⊢ H (⟨U, V⟩) = U H V$
18	17	a1i	$⊢ φ \to H (⟨U, V⟩) = U H V$
19	2	elexd	$⊢ φ \to U \in V$
20	3	elexd	$⊢ φ \to V \in V$
21		op1stg	$⊢ (U \in V \land V \in V) \to 1^{st} (⟨U, V⟩) = U$
22	19 20 21	syl2anc	$⊢ φ \to 1^{st} (⟨U, V⟩) = U$
23	22	fveq2d	$⊢ φ \to O (1^{st} (⟨U, V⟩)) = O (U)$
24		op2ndg	$⊢ (U \in V \land V \in V) \to 2^{nd} (⟨U, V⟩) = V$
25	19 20 24	syl2anc	$⊢ φ \to 2^{nd} (⟨U, V⟩) = V$
26	25	fveq2d	$⊢ φ \to O (2^{nd} (⟨U, V⟩)) = O (V)$
27	23 26	oveq12d	$⊢ φ \to O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩)) = O (U) N O (V)$
28	15 18 27	feq123d	$⊢ φ \to (P (⟨U, V⟩) : H (⟨U, V⟩) ⟶ O (1^{st} (⟨U, V⟩)) N O (2^{nd} (⟨U, V⟩)) \leftrightarrow (U P V) : U H V ⟶ O (U) N O (V))$
29	12 28	mpbid	$⊢ φ \to (U P V) : U H V ⟶ O (U) N O (V)$

Metamath Proof Explorer

Theorem ixpovf

Proof