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

Metamath Proof Explorer

Theorem initoval

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

Ref Expression
Hypotheses initoval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
initoval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion initoval ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )

Proof

Step Hyp Ref Expression
1 initoval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 initoval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 df-inito ⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
5 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6 5 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
8 7 3 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
9 8 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) = ( 𝑎 𝐻 𝑏 ) )
10 9 eleq2d ⊢ ( 𝑐 = 𝐶 → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
11 10 eubidv ⊢ ( 𝑐 = 𝐶 → ( ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
12 6 11 raleqbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
13 6 12 rabeqbidv ⊢ ( 𝑐 = 𝐶 → { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )
14 2 fvexi ⊢ 𝐵 ∈ V
15 14 rabex ⊢ { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } ∈ V
16 15 a1i ⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } ∈ V )
17 4 13 1 16 fvmptd3 ⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )