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

Metamath Proof Explorer

Theorem prstchomval

Description: Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
prstchomval.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
Assertion prstchomval ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 prstchomval.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
4 homid ⊢ Hom = Slot ( Hom ‘ ndx )
5 slotsbhcdif ⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
6 5 simp3i ⊢ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx )
7 1 2 4 6 prstcnidlem ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
8 fvex ⊢ ( le ‘ 𝐾 ) ∈ V
9 snex ⊢ { 1o } ∈ V
10 8 9 xpex ⊢ ( ( le ‘ 𝐾 ) × { 1o } ) ∈ V
11 4 setsid ⊢ ( ( 𝐾 ∈ Proset ∧ ( ( le ‘ 𝐾 ) × { 1o } ) ∈ V ) → ( ( le ‘ 𝐾 ) × { 1o } ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
12 2 10 11 sylancl ⊢ ( 𝜑 → ( ( le ‘ 𝐾 ) × { 1o } ) = ( Hom ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )
13 eqidd ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
14 1 2 13 prstcleval ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐶 ) )
15 14 3 eqtr4d ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ≤ )
16 15 xpeq1d ⊢ ( 𝜑 → ( ( le ‘ 𝐾 ) × { 1o } ) = ( ≤ × { 1o } ) )
17 7 12 16 3eqtr2rd ⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )