Metamath Proof Explorer

Theorem idfuval

Description: Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses idfuval.i ⊢ I = id func ⁡ C
idfuval.b ⊢ B = Base C
idfuval.c ⊢ φ → C ∈ Cat
idfuval.h ⊢ H = Hom ⁡ C
Assertion idfuval ⊢ φ → I = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢ I = id func ⁡ C
2 idfuval.b ⊢ B = Base C
3 idfuval.c ⊢ φ → C ∈ Cat
4 idfuval.h ⊢ H = Hom ⁡ C
5 fvexd ⊢ c = C → Base c ∈ V
6 fveq2 ⊢ c = C → Base c = Base C
7 6 2 eqtr4di ⊢ c = C → Base c = B
8 simpr ⊢ c = C ∧ b = B → b = B
9 8 reseq2d ⊢ c = C ∧ b = B → I ↾ b = I ↾ B
10 8 sqxpeqd ⊢ c = C ∧ b = B → b × b = B × B
11 simpl ⊢ c = C ∧ b = B → c = C
12 11 fveq2d ⊢ c = C ∧ b = B → Hom ⁡ c = Hom ⁡ C
13 12 4 eqtr4di ⊢ c = C ∧ b = B → Hom ⁡ c = H
14 13 fveq1d ⊢ c = C ∧ b = B → Hom ⁡ c ⁡ z = H ⁡ z
15 14 reseq2d ⊢ c = C ∧ b = B → I ↾ Hom ⁡ c ⁡ z = I ↾ H ⁡ z
16 10 15 mpteq12dv ⊢ c = C ∧ b = B → z ∈ b × b ⟼ I ↾ Hom ⁡ c ⁡ z = z ∈ B × B ⟼ I ↾ H ⁡ z
17 9 16 opeq12d ⊢ c = C ∧ b = B → I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ c ⁡ z = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
18 5 7 17 csbied2 ⊢ c = C → ⦋ Base c / b⦌ I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ c ⁡ z = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
19 df-idfu ⊢ id func = c ∈ Cat ⟼ ⦋ Base c / b⦌ I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ c ⁡ z
20 opex ⊢ I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z ∈ V
21 18 19 20 fvmpt ⊢ C ∈ Cat → id func ⁡ C = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
22 3 21 syl ⊢ φ → id func ⁡ C = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
23 1 22 syl5eq ⊢ φ → I = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z