Theorem fuco2el

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

	Ref	Expression
Assertion	fuco2el	⊢ ( ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) ↔ ( 𝐾 𝑆 𝐿 ∧ 𝐹 𝑅 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) ↔ ( ⟨ 𝐾 , 𝐿 ⟩ ∈ 𝑆 ∧ ⟨ 𝐹 , 𝐺 ⟩ ∈ 𝑅 ) )
2		df-br	⊢ ( 𝐾 𝑆 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ 𝑆 )
3		df-br	⊢ ( 𝐹 𝑅 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ 𝑅 )
4	2 3	anbi12i	⊢ ( ( 𝐾 𝑆 𝐿 ∧ 𝐹 𝑅 𝐺 ) ↔ ( ⟨ 𝐾 , 𝐿 ⟩ ∈ 𝑆 ∧ ⟨ 𝐹 , 𝐺 ⟩ ∈ 𝑅 ) )
5	1 4	bitr4i	⊢ ( ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) ↔ ( 𝐾 𝑆 𝐿 ∧ 𝐹 𝑅 𝐺 ) )