Description: An endomorphism in the parallel-arrow construction has the identity value. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 16-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | parhomval.h | ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ) | |
| parhomideq.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | ||
| parhomideq.e | ⊢ ( 𝜑 → 𝑈 = 𝑉 ) | ||
| Assertion | parhomideq | ⊢ ( 𝜑 → 𝐹 = 𝐽 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | parhomval.h | ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ) | |
| 2 | parhomideq.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | |
| 3 | parhomideq.e | ⊢ ( 𝜑 → 𝑈 = 𝑉 ) | |
| 4 | 3 | oveq2d | ⊢ ( 𝜑 → ( 𝑈 𝐻 𝑈 ) = ( 𝑈 𝐻 𝑉 ) ) |
| 5 | 2 4 | eleqtrrd | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑈 ) ) |
| 6 | 1 | elmpocl1 | ⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → 𝑈 ∈ 𝐵 ) |
| 7 | 1 | parhomidval | ⊢ ( 𝑈 ∈ 𝐵 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } ) |
| 8 | 2 6 7 | 3syl | ⊢ ( 𝜑 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } ) |
| 9 | 5 8 | eleqtrd | ⊢ ( 𝜑 → 𝐹 ∈ { 𝐽 } ) |
| 10 | 9 | elsnd | ⊢ ( 𝜑 → 𝐹 = 𝐽 ) |