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

Metamath Proof Explorer

Theorem prstcnidlem

Description: Lemma for prstcnid and prstchomval . (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
prstcnid.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
prstcnid.no ⊢ ( 𝐸 ‘ ndx ) ≠ ( comp ‘ ndx )
Assertion prstcnidlem ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 prstcnid.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4 prstcnid.no ⊢ ( 𝐸 ‘ ndx ) ≠ ( comp ‘ ndx )
5 1 2 prstcval ⊢ ( 𝜑 → 𝐶 = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
6 5 fveq2d ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) ) )
7 3 4 setsnid ⊢ ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
8 6 7 eqtr4di ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ) )