Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prstcnidlem Structured version   Visualization version   GIF version

Theorem prstcnidlem 49127
Description: Lemma for prstcnid 49128 and prstchomval 49136. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)
Hypotheses
Ref Expression
prstcnid.c (𝜑𝐶 = (ProsetToCat‘𝐾))
prstcnid.k (𝜑𝐾 ∈ Proset )
prstcnid.e 𝐸 = Slot (𝐸‘ndx)
prstcnid.no (𝐸‘ndx) ≠ (comp‘ndx)
Assertion
Ref Expression
prstcnidlem (𝜑 → (𝐸𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)))

Proof of Theorem prstcnidlem
StepHypRef Expression
1 prstcnid.c . . . 4 (𝜑𝐶 = (ProsetToCat‘𝐾))
2 prstcnid.k . . . 4 (𝜑𝐾 ∈ Proset )
31, 2prstcval 49126 . . 3 (𝜑𝐶 = ((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
43fveq2d 6908 . 2 (𝜑 → (𝐸𝐶) = (𝐸‘((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)))
5 prstcnid.e . . 3 𝐸 = Slot (𝐸‘ndx)
6 prstcnid.no . . 3 (𝐸‘ndx) ≠ (comp‘ndx)
75, 6setsnid 17241 . 2 (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)) = (𝐸‘((𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
84, 7eqtr4di 2794 1 (𝜑 → (𝐸𝐶) = (𝐸‘(𝐾 sSet ⟨(Hom ‘ndx), ((le‘𝐾) × {1o})⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  wne 2939  c0 4332  {csn 4624  cop 4630   × cxp 5681  cfv 6559  (class class class)co 7429  1oc1o 8495   sSet csts 17196  Slot cslot 17214  ndxcnx 17226  lecple 17300  Hom chom 17304  compcco 17305   Proset cproset 18334  ProsetToCatcprstc 49124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-res 5695  df-iota 6512  df-fun 6561  df-fv 6567  df-ov 7432  df-oprab 7433  df-mpo 7434  df-sets 17197  df-slot 17215  df-prstc 49125
This theorem is referenced by:  prstcnid  49128  prstchomval  49136
  Copyright terms: Public domain W3C validator