Description: Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prstcnid.c | No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
prstcnid.k | |
||
prstcnid.e | |
||
prstcnid.no | |
||
prstcnid.nh | |
||
Assertion | prstcnid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prstcnid.c | Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
2 | prstcnid.k | |
|
3 | prstcnid.e | |
|
4 | prstcnid.no | |
|
5 | prstcnid.nh | |
|
6 | 3 5 | setsnid | |
7 | 1 2 3 4 | prstcnidlem | |
8 | 6 7 | eqtr4id | |