1stfpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have same first projection functors. (Contributed by Zhi Wang, 20-Nov-2025)

	Ref	Expression
Hypotheses	1stfpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
	1stfpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
	1stfpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	1stfpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
	1stfpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
	1stfpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
	1stfpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	1stfpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	1stfpropd	⊢ ( 𝜑 → ( 𝐴 1^st_F 𝐶 ) = ( 𝐵 1^st_F 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		1stfpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		1stfpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		1stfpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
5		1stfpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
6		1stfpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
7		1stfpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8		1stfpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9	1 2 3 4 5 6 7 8	xpcpropd	⊢ ( 𝜑 → ( 𝐴 ×_c 𝐶 ) = ( 𝐵 ×_c 𝐷 ) )
10	9	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) = ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) )
11	10	reseq2d	⊢ ( 𝜑 → ( 1^st ↾ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ) = ( 1^st ↾ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ) )
12	9	fveq2d	⊢ ( 𝜑 → ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) )
13	12	oveqd	⊢ ( 𝜑 → ( 𝑥 ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) 𝑦 ) )
14	13	reseq2d	⊢ ( 𝜑 → ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) = ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) 𝑦 ) ) )
15	10 10 14	mpoeq123dv	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) 𝑦 ) ) ) )
16	11 15	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ↾ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ) , ( 𝑥 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 1^st ↾ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ) , ( 𝑥 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) 𝑦 ) ) ) ⟩ )
17		eqid	⊢ ( 𝐴 ×_c 𝐶 ) = ( 𝐴 ×_c 𝐶 )
18		eqid	⊢ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) = ( Base ‘ ( 𝐴 ×_c 𝐶 ) )
19		eqid	⊢ ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( Hom ‘ ( 𝐴 ×_c 𝐶 ) )
20		eqid	⊢ ( 𝐴 1^st_F 𝐶 ) = ( 𝐴 1^st_F 𝐶 )
21	17 18 19 5 7 20	1stfval	⊢ ( 𝜑 → ( 𝐴 1^st_F 𝐶 ) = ⟨ ( 1^st ↾ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ) , ( 𝑥 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐴 ×_c 𝐶 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ) ⟩ )
22		eqid	⊢ ( 𝐵 ×_c 𝐷 ) = ( 𝐵 ×_c 𝐷 )
23		eqid	⊢ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) = ( Base ‘ ( 𝐵 ×_c 𝐷 ) )
24		eqid	⊢ ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐵 ×_c 𝐷 ) )
25		eqid	⊢ ( 𝐵 1^st_F 𝐷 ) = ( 𝐵 1^st_F 𝐷 )
26	22 23 24 6 8 25	1stfval	⊢ ( 𝜑 → ( 𝐵 1^st_F 𝐷 ) = ⟨ ( 1^st ↾ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ) , ( 𝑥 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) , 𝑦 ∈ ( Base ‘ ( 𝐵 ×_c 𝐷 ) ) ↦ ( 1^st ↾ ( 𝑥 ( Hom ‘ ( 𝐵 ×_c 𝐷 ) ) 𝑦 ) ) ) ⟩ )
27	16 21 26	3eqtr4d	⊢ ( 𝜑 → ( 𝐴 1^st_F 𝐶 ) = ( 𝐵 1^st_F 𝐷 ) )

Metamath Proof Explorer

Theorem 1stfpropd

Proof