Metamath Proof Explorer

Theorem dmcoass

Description: The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses coafval.o ⊢ · ˙ = comp a ⁡ C
coafval.a ⊢ A = Arrow ⁡ C
Assertion dmcoass ⊢ dom ⁡ · ˙ ⊆ A × A

Proof

Step Hyp Ref Expression
1 coafval.o ⊢ · ˙ = comp a ⁡ C
2 coafval.a ⊢ A = Arrow ⁡ C
3 eqid ⊢ comp ⁡ C = comp ⁡ C
4 1 2 3 coafval ⊢ · ˙ = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ C cod a ⁡ g 2 nd ⁡ f
5 4 dmmpossx ⊢ dom ⁡ · ˙ ⊆ ⋃ g ∈ A g × h ∈ A | cod a ⁡ h = dom a ⁡ g
6 iunss ⊢ ⋃ g ∈ A g × h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A × A ↔ ∀ g ∈ A g × h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A × A
7 snssi ⊢ g ∈ A → g ⊆ A
8 ssrab2 ⊢ h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A
9 xpss12 ⊢ g ⊆ A ∧ h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A → g × h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A × A
10 7 8 9 sylancl ⊢ g ∈ A → g × h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A × A
11 6 10 mprgbir ⊢ ⋃ g ∈ A g × h ∈ A | cod a ⁡ h = dom a ⁡ g ⊆ A × A
12 5 11 sstri ⊢ dom ⁡ · ˙ ⊆ A × A