Description: Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | homarcl.h | ⊢ 𝐻 = ( Homa ‘ 𝐶 ) | |
Assertion | homarcl | ⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | homarcl.h | ⊢ 𝐻 = ( Homa ‘ 𝐶 ) | |
2 | n0i | ⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ ) | |
3 | df-homa | ⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) ) | |
4 | 3 | fvmptndm | ⊢ ( ¬ 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ∅ ) |
5 | 1 4 | eqtrid | ⊢ ( ¬ 𝐶 ∈ Cat → 𝐻 = ∅ ) |
6 | 5 | oveqd | ⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ∅ 𝑌 ) ) |
7 | 0ov | ⊢ ( 𝑋 ∅ 𝑌 ) = ∅ | |
8 | 6 7 | eqtrdi | ⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑋 𝐻 𝑌 ) = ∅ ) |
9 | 2 8 | nsyl2 | ⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat ) |