fuco2el

Description: Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025)

		Ref	Expression
	Assertion	fuco2el	$⊢ ⟨⟨K, L⟩, ⟨F, G⟩⟩ \in (S \times R) \leftrightarrow (K S L \land F R G)$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨⟨K, L⟩, ⟨F, G⟩⟩ \in (S \times R) \leftrightarrow (⟨K, L⟩ \in S \land ⟨F, G⟩ \in R)$
2		df-br	$⊢ K S L \leftrightarrow ⟨K, L⟩ \in S$
3		df-br	$⊢ F R G \leftrightarrow ⟨F, G⟩ \in R$
4	2 3	anbi12i	$⊢ (K S L \land F R G) \leftrightarrow (⟨K, L⟩ \in S \land ⟨F, G⟩ \in R)$
5	1 4	bitr4i	$⊢ ⟨⟨K, L⟩, ⟨F, G⟩⟩ \in (S \times R) \leftrightarrow (K S L \land F R G)$

Metamath Proof Explorer