Theorem fuco2eld

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

	Ref	Expression
Hypotheses	fuco2eld.w	⊢ ( 𝜑 → 𝑊 = ( 𝑆 × 𝑅 ) )
	fuco2eld.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
	fuco2eld.k	⊢ ( 𝜑 → 𝐾 𝑆 𝐿 )
	fuco2eld.f	⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
Assertion	fuco2eld	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	⊢ ( 𝜑 → 𝑊 = ( 𝑆 × 𝑅 ) )
2		fuco2eld.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
3		fuco2eld.k	⊢ ( 𝜑 → 𝐾 𝑆 𝐿 )
4		fuco2eld.f	⊢ ( 𝜑 → 𝐹 𝑅 𝐺 )
5		fuco2el	⊢ ( ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) ↔ ( 𝐾 𝑆 𝐿 ∧ 𝐹 𝑅 𝐺 ) )
6	3 4 5	sylanbrc	⊢ ( 𝜑 → ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) )
7	6 2 1	3eltr4d	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )