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	⊢ · = ( comp_a ‘ 𝐶 )
	coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
Assertion	eldmcoa	⊢ ( 𝐺 dom · 𝐹 ↔ ( 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coafval.o	⊢ · = ( comp_a ‘ 𝐶 )
2		coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
3		df-br	⊢ ( 𝐺 dom · 𝐹 ↔ ⟨ 𝐺 , 𝐹 ⟩ ∈ dom · )
4		otex	⊢ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ V
5	4	rgen2w	⊢ ∀ 𝑔 ∈ 𝐴 ∀ 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ V
6		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7	1 2 6	coafval	⊢ · = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
8	7	fmpox	⊢ ( ∀ 𝑔 ∈ 𝐴 ∀ 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ V ↔ · : ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ) ⟶ V )
9	5 8	mpbi	⊢ · : ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ) ⟶ V
10	9	fdmi	⊢ dom · = ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } )
11	10	eleq2i	⊢ ( ⟨ 𝐺 , 𝐹 ⟩ ∈ dom · ↔ ⟨ 𝐺 , 𝐹 ⟩ ∈ ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ) )
12		fveq2	⊢ ( 𝑔 = 𝐺 → ( dom_a ‘ 𝑔 ) = ( dom_a ‘ 𝐺 ) )
13	12	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) ↔ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) ) )
14	13	rabbidv	⊢ ( 𝑔 = 𝐺 → { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } = { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) } )
15	14	opeliunxp2	⊢ ( ⟨ 𝐺 , 𝐹 ⟩ ∈ ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ) ↔ ( 𝐺 ∈ 𝐴 ∧ 𝐹 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) } ) )
16		fveqeq2	⊢ ( ℎ = 𝐹 → ( ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) ↔ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )
17	16	elrab	⊢ ( 𝐹 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) } ↔ ( 𝐹 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )
18	17	anbi2i	⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝐹 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝐺 ) } ) ↔ ( 𝐺 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ) )
19		an12	⊢ ( ( 𝐺 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ) ↔ ( 𝐹 ∈ 𝐴 ∧ ( 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ) )
20		3anass	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ↔ ( 𝐹 ∈ 𝐴 ∧ ( 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ) )
21	19 20	bitr4i	⊢ ( ( 𝐺 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) ) ↔ ( 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )
22	15 18 21	3bitri	⊢ ( ⟨ 𝐺 , 𝐹 ⟩ ∈ ∪ 𝑔 ∈ 𝐴 ( { 𝑔 } × { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ) ↔ ( 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )
23	3 11 22	3bitri	⊢ ( 𝐺 dom · 𝐹 ↔ ( 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ ( cod_a ‘ 𝐹 ) = ( dom_a ‘ 𝐺 ) ) )

Metamath Proof Explorer

Theorem eldmcoa

Proof