fuco2eld2

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	fuco2eld2	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		fuco2eld.w	⊢ ( 𝜑 → 𝑊 = ( 𝑆 × 𝑅 ) )
2		fuco2eld2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
3		fuco2eld2.s	⊢ Rel 𝑆
4		fuco2eld2.r	⊢ Rel 𝑅
5	2 1	eleqtrd	⊢ ( 𝜑 → 𝑈 ∈ ( 𝑆 × 𝑅 ) )
6		1st2nd2	⊢ ( 𝑈 ∈ ( 𝑆 × 𝑅 ) → 𝑈 = ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ )
7	5 6	syl	⊢ ( 𝜑 → 𝑈 = ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ )
8		df-rel	⊢ ( Rel 𝑆 ↔ 𝑆 ⊆ ( V × V ) )
9	3 8	mpbi	⊢ 𝑆 ⊆ ( V × V )
10		xp1st	⊢ ( 𝑈 ∈ ( 𝑆 × 𝑅 ) → ( 1^st ‘ 𝑈 ) ∈ 𝑆 )
11	9 10	sselid	⊢ ( 𝑈 ∈ ( 𝑆 × 𝑅 ) → ( 1^st ‘ 𝑈 ) ∈ ( V × V ) )
12		1st2nd2	⊢ ( ( 1^st ‘ 𝑈 ) ∈ ( V × V ) → ( 1^st ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ )
13	5 11 12	3syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ )
14		df-rel	⊢ ( Rel 𝑅 ↔ 𝑅 ⊆ ( V × V ) )
15	4 14	mpbi	⊢ 𝑅 ⊆ ( V × V )
16		xp2nd	⊢ ( 𝑈 ∈ ( 𝑆 × 𝑅 ) → ( 2^nd ‘ 𝑈 ) ∈ 𝑅 )
17	15 16	sselid	⊢ ( 𝑈 ∈ ( 𝑆 × 𝑅 ) → ( 2^nd ‘ 𝑈 ) ∈ ( V × V ) )
18		1st2nd2	⊢ ( ( 2^nd ‘ 𝑈 ) ∈ ( V × V ) → ( 2^nd ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ )
19	5 17 18	3syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ )
20	13 19	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )
21	7 20	eqtrd	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )

Metamath Proof Explorer

Theorem fuco2eld2

Proof