Theorem relfunc

Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	relfunc	⊢ Rel ( 𝐷 Func 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		df-func	⊢ Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
2	1	relmpoopab	⊢ Rel ( 𝐷 Func 𝐸 )