This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relfunc

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

Ref Expression
Assertion relfunc ⊢ Rel ⁡ D Func E

Proof

Step Hyp Ref Expression
1 df-func ⊢ Func = t ∈ Cat , u ∈ Cat ⟼ f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
2 1 relmpoopab ⊢ Rel ⁡ D Func E