funcf2lem

Description: A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Assertion	funcf2lem	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (B \times B) \land \forall x \in B \forall y \in B (x G y) : x H y ⟶ F (x) J F (y))$

Proof

Step	Hyp	Ref	Expression
1		elixp2	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (B \times B) \land \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}))$
2		fveq2	$⊢ z = ⟨x, y⟩ \to G (z) = G (⟨x, y⟩)$
3		df-ov	$⊢ x G y = G (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ z = ⟨x, y⟩ \to G (z) = x G y$
5		vex	$⊢ x \in V$
6		vex	$⊢ y \in V$
7	5 6	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
8	7	fveq2d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) = F (x)$
9	5 6	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
10	9	fveq2d	$⊢ z = ⟨x, y⟩ \to F (2^{nd} (z)) = F (y)$
11	8 10	oveq12d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) J F (2^{nd} (z)) = F (x) J F (y)$
12		fveq2	$⊢ z = ⟨x, y⟩ \to H (z) = H (⟨x, y⟩)$
13		df-ov	$⊢ x H y = H (⟨x, y⟩)$
14	12 13	eqtr4di	$⊢ z = ⟨x, y⟩ \to H (z) = x H y$
15	11 14	oveq12d	$⊢ z = ⟨x, y⟩ \to {(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)} = {(F (x) J F (y))}^{(x H y)}$
16	4 15	eleq12d	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow x G y \in ({(F (x) J F (y))}^{(x H y)}))$
17		ovex	$⊢ F (x) J F (y) \in V$
18		ovex	$⊢ x H y \in V$
19	17 18	elmap	$⊢ x G y \in ({(F (x) J F (y))}^{(x H y)}) \leftrightarrow (x G y) : x H y ⟶ F (x) J F (y)$
20	16 19	bitrdi	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (x G y) : x H y ⟶ F (x) J F (y))$
21	20	ralxp	$⊢ \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow \forall x \in B \forall y \in B (x G y) : x H y ⟶ F (x) J F (y)$
22	21	3anbi3i	$⊢ (G \in V \land G Fn (B \times B) \land \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})) \leftrightarrow (G \in V \land G Fn (B \times B) \land \forall x \in B \forall y \in B (x G y) : x H y ⟶ F (x) J F (y))$
23	1 22	bitri	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (B \times B) \land \forall x \in B \forall y \in B (x G y) : x H y ⟶ F (x) J F (y))$

Metamath Proof Explorer

Theorem funcf2lem

Proof