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

Metamath Proof Explorer

Theorem imaidfu2lem

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

Ref Expression
Hypotheses imaidfu.i ⊢ I = id func ⁡ C
imaidfu.d ⊢ φ → I ∈ D Func E
Assertion imaidfu2lem ⊢ φ → 1 st ⁡ I Base D = Base D

Proof

Step Hyp Ref Expression
1 imaidfu.i ⊢ I = id func ⁡ C
2 imaidfu.d ⊢ φ → I ∈ D Func E
3 eqidd ⊢ φ → Base D = Base D
4 1 2 3 idfu1sta ⊢ φ → 1 st ⁡ I = I ↾ Base D
5 4 imaeq1d ⊢ φ → 1 st ⁡ I Base D = I ↾ Base D Base D
6 ssid ⊢ Base D ⊆ Base D
7 resiima ⊢ Base D ⊆ Base D → I ↾ Base D Base D = Base D
8 6 7 ax-mp ⊢ I ↾ Base D Base D = Base D
9 5 8 eqtrdi ⊢ φ → 1 st ⁡ I Base D = Base D