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	⊢ · = ( compa ‘ 𝐶 )
	coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
Assertion	dmcoass	⊢ dom · ⊆ ( 𝐴 × 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		coafval.o	⊢ · = ( compa ‘ 𝐶 )
2		coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
3		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
4	1 2 3	coafval	⊢ · = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ )
5	4	dmmpossx	⊢ dom · ⊆ ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } )
6		iunss	⊢ ( ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ) ⊆ ( 𝐴 × 𝐴 ) ↔ ∀ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ) ⊆ ( 𝐴 × 𝐴 ) )
7		snssi	⊢ ( 𝑔 ∈ 𝐴 → { 𝑔 } ⊆ 𝐴 )
8		ssrab2	⊢ { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ⊆ 𝐴
9		xpss12	⊢ ( ( { 𝑔 } ⊆ 𝐴 ∧ { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ⊆ 𝐴 ) → ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ) ⊆ ( 𝐴 × 𝐴 ) )
10	7 8 9	sylancl	⊢ ( 𝑔 ∈ 𝐴 → ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ) ⊆ ( 𝐴 × 𝐴 ) )
11	6 10	mprgbir	⊢ ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ) ⊆ ( 𝐴 × 𝐴 )
12	5 11	sstri	⊢ dom · ⊆ ( 𝐴 × 𝐴 )