Description: When every member of the parallel-arrow class S is a subset of J , every arrow in a hom-set is a subset of its identity value J . The subset hypothesis is essential; it does not follow from the hom-set definition alone. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | parhomval.h | ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ) | |
| parhomss.p | ⊢ 𝑆 ⊆ 𝒫 𝐽 | ||
| parhomss.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | ||
| Assertion | parhomss | ⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | parhomval.h | ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ) | |
| 2 | parhomss.p | ⊢ 𝑆 ⊆ 𝒫 𝐽 | |
| 3 | parhomss.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | |
| 4 | snsspw | ⊢ { 𝐽 } ⊆ 𝒫 𝐽 | |
| 5 | 2 4 | unssi | ⊢ ( 𝑆 ∪ { 𝐽 } ) ⊆ 𝒫 𝐽 |
| 6 | eqid | ⊢ ( 𝑆 ∪ { 𝐽 } ) = ( 𝑆 ∪ { 𝐽 } ) | |
| 7 | 1 6 3 | parhomcl | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 ∪ { 𝐽 } ) ) |
| 8 | 5 7 | sselid | ⊢ ( 𝜑 → 𝐹 ∈ 𝒫 𝐽 ) |
| 9 | 8 | elpwid | ⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 ) |