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 ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstchomval.l ⊢ φ → ≤ ˙ = ≤ C
Assertion prstchomval ⊢ φ → ≤ ˙ × 1 𝑜 = Hom ⁡ C

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 prstchomval.l ⊢ φ → ≤ ˙ = ≤ C
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 ⁡ C = Hom ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜
8 fvex ⊢ ≤ K ∈ V
9 snex ⊢ 1 𝑜 ∈ V
10 8 9 xpex ⊢ ≤ K × 1 𝑜 ∈ V
11 4 setsid ⊢ K ∈ Proset ∧ ≤ K × 1 𝑜 ∈ V → ≤ K × 1 𝑜 = Hom ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜
12 2 10 11 sylancl ⊢ φ → ≤ K × 1 𝑜 = Hom ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜
13 eqidd ⊢ φ → ≤ K = ≤ K
14 1 2 13 prstcleval ⊢ φ → ≤ K = ≤ C
15 14 3 eqtr4d ⊢ φ → ≤ K = ≤ ˙
16 15 xpeq1d ⊢ φ → ≤ K × 1 𝑜 = ≤ ˙ × 1 𝑜
17 7 12 16 3eqtr2rd ⊢ φ → ≤ ˙ × 1 𝑜 = Hom ⁡ C