Metamath Proof Explorer

Theorem initoid

Description: For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 6-Apr-2020)

Ref Expression
Hypotheses isinitoi.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isinitoi.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isinitoi.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion initoid ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } )

Proof

Step Hyp Ref Expression
1 isinitoi.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isinitoi.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isinitoi.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 1 2 3 isinitoi ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ 𝐵 ∧ ∀ 𝑜 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) ) )
5 oveq2 ⊢ ( 𝑜 = 𝑂 → ( 𝑂 𝐻 𝑜 ) = ( 𝑂 𝐻 𝑂 ) )
6 5 eleq2d ⊢ ( 𝑜 = 𝑂 → ( ℎ ∈ ( 𝑂 𝐻 𝑜 ) ↔ ℎ ∈ ( 𝑂 𝐻 𝑂 ) ) )
7 6 eubidv ⊢ ( 𝑜 = 𝑂 → ( ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) ↔ ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑂 ) ) )
8 7 rspcv ⊢ ( 𝑂 ∈ 𝐵 → ( ∀ 𝑜 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) → ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑂 ) ) )
9 8 adantl ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( ∀ 𝑜 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) → ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑂 ) ) )
10 eusn ⊢ ( ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑂 ) ↔ ∃ ℎ ( 𝑂 𝐻 𝑂 ) = { ℎ } )
11 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → 𝐶 ∈ Cat )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → 𝑂 ∈ 𝐵 )
14 1 2 11 12 13 catidcl ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ ( 𝑂 𝐻 𝑂 ) )
15 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ V
16 15 elsn ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ { ℎ } ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) = ℎ )
17 eqcom ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) = ℎ ↔ ℎ = ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) )
18 sneqbg ⊢ ( ℎ ∈ V → ( { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ↔ ℎ = ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ) )
19 18 bicomd ⊢ ( ℎ ∈ V → ( ℎ = ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ↔ { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
20 19 elv ⊢ ( ℎ = ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ↔ { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } )
21 16 17 20 3bitri ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ { ℎ } ↔ { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } )
22 21 biimpi ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ { ℎ } → { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } )
23 22 a1i ⊢ ( ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ { ℎ } → { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
24 eleq2 ⊢ ( ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ ( 𝑂 𝐻 𝑂 ) ↔ ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ { ℎ } ) )
25 eqeq1 ⊢ ( ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ↔ { ℎ } = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
26 23 24 25 3imtr4d ⊢ ( ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ ( 𝑂 𝐻 𝑂 ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
27 14 26 syl5 ⊢ ( ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
28 27 exlimiv ⊢ ( ∃ ℎ ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
29 28 com12 ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( ∃ ℎ ( 𝑂 𝐻 𝑂 ) = { ℎ } → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
30 10 29 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑂 ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
31 9 30 syld ⊢ ( ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) ∧ 𝑂 ∈ 𝐵 ) → ( ∀ 𝑜 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
32 31 expimpd ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( ( 𝑂 ∈ 𝐵 ∧ ∀ 𝑜 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑜 ) ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } ) )
33 4 32 mpd ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 𝐻 𝑂 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) } )