fuco2eld2

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

Step	Hyp	Ref	Expression
1		fuco2eld.w	$⊢ φ \to W = S \times R$
2		fuco2eld2.u	$⊢ φ \to U \in W$
3		fuco2eld2.s	$⊢ Rel S$
4		fuco2eld2.r	$⊢ Rel R$
5	2 1	eleqtrd	$⊢ φ \to U \in (S \times R)$
6		1st2nd2	$⊢ U \in (S \times R) \to U = ⟨1^{st} (U), 2^{nd} (U)⟩$
7	5 6	syl	$⊢ φ \to U = ⟨1^{st} (U), 2^{nd} (U)⟩$
8		df-rel	$⊢ Rel S \leftrightarrow S \subseteq V \times V$
9	3 8	mpbi	$⊢ S \subseteq V \times V$
10		xp1st	$⊢ U \in (S \times R) \to 1^{st} (U) \in S$
11	9 10	sselid	$⊢ U \in (S \times R) \to 1^{st} (U) \in (V \times V)$
12		1st2nd2	$⊢ 1^{st} (U) \in (V \times V) \to 1^{st} (U) = ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩$
13	5 11 12	3syl	$⊢ φ \to 1^{st} (U) = ⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩$
14		df-rel	$⊢ Rel R \leftrightarrow R \subseteq V \times V$
15	4 14	mpbi	$⊢ R \subseteq V \times V$
16		xp2nd	$⊢ U \in (S \times R) \to 2^{nd} (U) \in R$
17	15 16	sselid	$⊢ U \in (S \times R) \to 2^{nd} (U) \in (V \times V)$
18		1st2nd2	$⊢ 2^{nd} (U) \in (V \times V) \to 2^{nd} (U) = ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩$
19	5 17 18	3syl	$⊢ φ \to 2^{nd} (U) = ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩$
20	13 19	opeq12d	$⊢ φ \to ⟨1^{st} (U), 2^{nd} (U)⟩ = ⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩$
21	7 20	eqtrd	$⊢ φ \to U = ⟨⟨1^{st} (1^{st} (U)), 2^{nd} (1^{st} (U))⟩, ⟨1^{st} (2^{nd} (U)), 2^{nd} (2^{nd} (U))⟩⟩$

Metamath Proof Explorer