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

Metamath Proof Explorer

Theorem reldmfunc

Description: The domain of Func is a relation. (Contributed by Zhi Wang, 12-Nov-2025)

Ref Expression
Assertion reldmfunc ⊢ Rel ⁡ dom ⁡ Func

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 reldmmpo ⊢ Rel ⁡ dom ⁡ Func