Theorem eldmcoa

Description: A pair <. G , F >. is in the domain of the arrow composition, if the domain of G equals the codomain of F . (In this case we say G and F are composable.) (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	coafval.o	|- .x. = ( compA ` C )
	coafval.a	|- A = ( Arrow ` C )
Assertion	eldmcoa	|- ( G dom .x. F <-> ( F e. A /\ G e. A /\ ( codA ` F ) = ( domA ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		coafval.o	|- .x. = ( compA ` C )
2		coafval.a	|- A = ( Arrow ` C )
3		df-br	|- ( G dom .x. F <-> <. G , F >. e. dom .x. )
4		otex	|- <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` C ) ( codA ` g ) ) ( 2nd ` f ) ) >. e. _V
5	4	rgen2w	|- A. g e. A 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 ) ) >. e. _V
6		eqid	|- ( comp ` C ) = ( comp ` C )
7	1 2 6	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 ) ) >. )
8	7	fmpox	|- ( A. g e. A 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 ) ) >. e. _V <-> .x. : U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) --> _V )
9	5 8	mpbi	|- .x. : U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) --> _V
10	9	fdmi	|- dom .x. = U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } )
11	10	eleq2i	|- ( <. G , F >. e. dom .x. <-> <. G , F >. e. U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) )
12		fveq2	|- ( g = G -> ( domA ` g ) = ( domA ` G ) )
13	12	eqeq2d	|- ( g = G -> ( ( codA ` h ) = ( domA ` g ) <-> ( codA ` h ) = ( domA ` G ) ) )
14	13	rabbidv	|- ( g = G -> { h e. A | ( codA ` h ) = ( domA ` g ) } = { h e. A | ( codA ` h ) = ( domA ` G ) } )
15	14	opeliunxp2	|- ( <. G , F >. e. U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) <-> ( G e. A /\ F e. { h e. A | ( codA ` h ) = ( domA ` G ) } ) )
16		fveqeq2	|- ( h = F -> ( ( codA ` h ) = ( domA ` G ) <-> ( codA ` F ) = ( domA ` G ) ) )
17	16	elrab	|- ( F e. { h e. A | ( codA ` h ) = ( domA ` G ) } <-> ( F e. A /\ ( codA ` F ) = ( domA ` G ) ) )
18	17	anbi2i	|- ( ( G e. A /\ F e. { h e. A | ( codA ` h ) = ( domA ` G ) } ) <-> ( G e. A /\ ( F e. A /\ ( codA ` F ) = ( domA ` G ) ) ) )
19		an12	|- ( ( G e. A /\ ( F e. A /\ ( codA ` F ) = ( domA ` G ) ) ) <-> ( F e. A /\ ( G e. A /\ ( codA ` F ) = ( domA ` G ) ) ) )
20		3anass	|- ( ( F e. A /\ G e. A /\ ( codA ` F ) = ( domA ` G ) ) <-> ( F e. A /\ ( G e. A /\ ( codA ` F ) = ( domA ` G ) ) ) )
21	19 20	bitr4i	|- ( ( G e. A /\ ( F e. A /\ ( codA ` F ) = ( domA ` G ) ) ) <-> ( F e. A /\ G e. A /\ ( codA ` F ) = ( domA ` G ) ) )
22	15 18 21	3bitri	|- ( <. G , F >. e. U_ g e. A ( { g } X. { h e. A | ( codA ` h ) = ( domA ` g ) } ) <-> ( F e. A /\ G e. A /\ ( codA ` F ) = ( domA ` G ) ) )
23	3 11 22	3bitri	|- ( G dom .x. F <-> ( F e. A /\ G e. A /\ ( codA ` F ) = ( domA ` G ) ) )