Metamath Proof Explorer

Theorem termoval

Description: The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses initoval.c ⊢ φ → C ∈ Cat
initoval.b ⊢ B = Base C
initoval.h ⊢ H = Hom ⁡ C
Assertion termoval ⊢ φ → TermO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a

Proof

Step Hyp Ref Expression
1 initoval.c ⊢ φ → C ∈ Cat
2 initoval.b ⊢ B = Base C
3 initoval.h ⊢ H = Hom ⁡ C
4 df-termo ⊢ TermO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
5 fveq2 ⊢ c = C → Base c = Base C
6 5 2 eqtr4di ⊢ c = C → Base c = B
7 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
8 7 3 eqtr4di ⊢ c = C → Hom ⁡ c = H
9 8 oveqd ⊢ c = C → b Hom ⁡ c a = b H a
10 9 eleq2d ⊢ c = C → h ∈ b Hom ⁡ c a ↔ h ∈ b H a
11 10 eubidv ⊢ c = C → ∃! h h ∈ b Hom ⁡ c a ↔ ∃! h h ∈ b H a
12 6 11 raleqbidv ⊢ c = C → ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a ↔ ∀ b ∈ B ∃! h h ∈ b H a
13 6 12 rabeqbidv ⊢ c = C → a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a = a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a
14 2 fvexi ⊢ B ∈ V
15 14 rabex ⊢ a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a ∈ V
16 15 a1i ⊢ φ → a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a ∈ V
17 4 13 1 16 fvmptd3 ⊢ φ → TermO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a