This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idfu1stalem

Description: Lemma for idfu1sta . (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses idfu2nda.i ⊢ I = id func ⁡ C
idfu2nda.d ⊢ φ → I ∈ D Func E
idfu2nda.b ⊢ φ → B = Base D
Assertion idfu1stalem ⊢ φ → B = Base C

Proof

Step Hyp Ref Expression
1 idfu2nda.i ⊢ I = id func ⁡ C
2 idfu2nda.d ⊢ φ → I ∈ D Func E
3 idfu2nda.b ⊢ φ → B = Base D
4 1 2 eqeltrrid ⊢ φ → id func ⁡ C ∈ D Func E
5 idfurcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat
6 1 idfucl ⊢ C ∈ Cat → I ∈ C Func C
7 4 5 6 3syl ⊢ φ → I ∈ C Func C
8 7 func1st2nd ⊢ φ → 1 st ⁡ I C Func C 2 nd ⁡ I
9 2 func1st2nd ⊢ φ → 1 st ⁡ I D Func E 2 nd ⁡ I
10 8 9 funchomf ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
11 10 homfeqbas ⊢ φ → Base C = Base D
12 3 11 eqtr4d ⊢ φ → B = Base C