Theorem fuco2eld3

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

	Ref	Expression
Hypotheses	fuco2eld.w	⊢ ( 𝜑 → 𝑊 = ( 𝑆 × 𝑅 ) )
	fuco2eld2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	fuco2eld2.s	⊢ Rel 𝑆
	fuco2eld2.r	⊢ Rel 𝑅
Assertion	fuco2eld3	⊢ ( 𝜑 → ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∧ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) 𝑅 ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	⊢ ( 𝜑 → 𝑊 = ( 𝑆 × 𝑅 ) )
2		fuco2eld2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
3		fuco2eld2.s	⊢ Rel 𝑆
4		fuco2eld2.r	⊢ Rel 𝑅
5	1 2 3 4	fuco2eld2	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) , ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ⟩ ⟩ )
6	2 5 1	3eltr3d	⊢ ( 𝜑 → ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) , ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) )
7		fuco2el	⊢ ( ⟨ ⟨ ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) , ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ⟩ ⟩ ∈ ( 𝑆 × 𝑅 ) ↔ ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∧ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) 𝑅 ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ) )
8	6 7	sylib	⊢ ( 𝜑 → ( ( 1st ‘ ( 1st ‘ 𝑈 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ∧ ( 1st ‘ ( 2nd ‘ 𝑈 ) ) 𝑅 ( 2nd ‘ ( 2nd ‘ 𝑈 ) ) ) )