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 
|- .x. = ( compA ` C )
coafval.a 
|- A = ( Arrow ` C )
Assertion dmcoass 
|- dom .x. C_ ( A X. A )

Proof

Step Hyp Ref Expression
1 coafval.o 
 |-  .x. = ( compA ` C )
2 coafval.a 
 |-  A = ( Arrow ` C )
3 eqid 
 |-  ( comp ` C ) = ( comp ` C )
4 1 2 3 coafval 
 |-  .x. = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` C ) ( codA ` g ) ) ( 2nd ` f ) ) >. )
5 4 dmmpossx 
 |-  dom .x. C_ U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } )
6 iunss 
 |-  ( U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) C_ ( A X. A ) <-> A. g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) C_ ( A X. A ) )
7 snssi 
 |-  ( g e. A -> { g } C_ A )
8 ssrab2 
 |-  { h e. A | ( codA ` h ) = ( domA ` g ) } C_ A
9 xpss12 
 |-  ( ( { g } C_ A /\ { h e. A | ( codA ` h ) = ( domA ` g ) } C_ A ) -> ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) C_ ( A X. A ) )
10 7 8 9 sylancl 
 |-  ( g e. A -> ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) C_ ( A X. A ) )
11 6 10 mprgbir 
 |-  U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) C_ ( A X. A )
12 5 11 sstri 
 |-  dom .x. C_ ( A X. A )