Description: Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT ). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | prstcnid.c | ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) ) | |
| prstcnid.k | ⊢ ( 𝜑 → 𝐾 ∈ Proset ) | ||
| prstchom.l | ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) ) | ||
| prstchom.e | ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) ) | ||
| prstchom.x | ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) ) | ||
| prstchom.y | ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) ) | ||
| Assertion | prstchom2 | ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prstcnid.c | ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) ) | |
| 2 | prstcnid.k | ⊢ ( 𝜑 → 𝐾 ∈ Proset ) | |
| 3 | prstchom.l | ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) ) | |
| 4 | prstchom.e | ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) ) | |
| 5 | prstchom.x | ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) ) | |
| 6 | prstchom.y | ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) ) | |
| 7 | 1 2 3 4 5 6 | prstchom | ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) ) |
| 8 | 1 2 | prstcthin | ⊢ ( 𝜑 → 𝐶 ∈ ThinCat ) |
| 9 | eqidd | ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) ) | |
| 10 | 8 5 6 9 4 | thincn0eu | ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) ) |
| 11 | 7 10 | bitrd | ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) ) |