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 ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
idfu2nda.d ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
idfu2nda.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
Assertion idfu1stalem ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 idfu2nda.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 idfu2nda.d ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
3 idfu2nda.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
4 1 2 eqeltrrid ⊢ ( 𝜑 → ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) )
5 idfurcl ⊢ ( ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) → 𝐶 ∈ Cat )
6 1 idfucl ⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
7 4 5 6 3syl ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
8 7 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) )
9 2 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐼 ) )
10 8 9 funchomf ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
11 10 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
12 3 11 eqtr4d ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )