Theorem homarcl2

Description: Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homarcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	homarcl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		homarcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		elfvdm	⊢ ( 𝐹 ∈ ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐻 )
4		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5	3 4	eleq2s	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐻 )
6	1	homarcl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
7	1 2 6	homaf	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐻 : ( 𝐵 × 𝐵 ) ⟶ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )
8	7	fdmd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → dom 𝐻 = ( 𝐵 × 𝐵 ) )
9	5 8	eleqtrd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
10		opelxp	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
11	9 10	sylib	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )