eldmcoa - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eldmcoa		Structured version Visualization version GIF version

Theorem eldmcoa 18011

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

**Hypotheses**
Ref	Expression
coafval.o	⊢ · = (comp_a‘𝐶)
coafval.a	⊢ 𝐴 = (Arrow‘𝐶)

**Assertion**
Ref	Expression
eldmcoa	⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)))

Proof of Theorem eldmcoa Dummy variables 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 5148	. 2 ⊢ (𝐺dom · 𝐹 ↔ ⟨𝐺, 𝐹⟩ ∈ dom · )
2		otex 5464	. . . . . 6 ⊢ ⟨(dom_a‘𝑓), (cod_a‘𝑔), ((2^nd ‘𝑔)(⟨(dom_a‘𝑓), (dom_a‘𝑔)⟩(comp‘𝐶)(cod_a‘𝑔))(2^nd ‘𝑓))⟩ ∈ V
3	2	rgen2w 3066	. . . . 5 ⊢ ∀𝑔 ∈ 𝐴 ∀𝑓 ∈ {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)}⟨(dom_a‘𝑓), (cod_a‘𝑔), ((2^nd ‘𝑔)(⟨(dom_a‘𝑓), (dom_a‘𝑔)⟩(comp‘𝐶)(cod_a‘𝑔))(2^nd ‘𝑓))⟩ ∈ V
4		coafval.o	. . . . . . 7 ⊢ · = (comp_a‘𝐶)
5		coafval.a	. . . . . . 7 ⊢ 𝐴 = (Arrow‘𝐶)
6		eqid 2732	. . . . . . 7 ⊢ (comp‘𝐶) = (comp‘𝐶)
7	4, 5, 6	coafval 18010	. . . . . 6 ⊢ · = (𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)} ↦ ⟨(dom_a‘𝑓), (cod_a‘𝑔), ((2^nd ‘𝑔)(⟨(dom_a‘𝑓), (dom_a‘𝑔)⟩(comp‘𝐶)(cod_a‘𝑔))(2^nd ‘𝑓))⟩)
8	7	fmpox 8049	. . . . 5 ⊢ (∀𝑔 ∈ 𝐴 ∀𝑓 ∈ {ℎ ∈ 𝐴 ∣ (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	3, 8	mpbi 229	. . . 4 ⊢ · :∪ 𝑔 ∈ 𝐴 ({𝑔} × {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)})⟶V
10	9	fdmi 6726	. . 3 ⊢ dom · = ∪ 𝑔 ∈ 𝐴 ({𝑔} × {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)})
11	10	eleq2i 2825	. 2 ⊢ (⟨𝐺, 𝐹⟩ ∈ dom · ↔ ⟨𝐺, 𝐹⟩ ∈ ∪ 𝑔 ∈ 𝐴 ({𝑔} × {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)}))
12		fveq2 6888	. . . . . 6 ⊢ (𝑔 = 𝐺 → (dom_a‘𝑔) = (dom_a‘𝐺))
13	12	eqeq2d 2743	. . . . 5 ⊢ (𝑔 = 𝐺 → ((cod_a‘ℎ) = (dom_a‘𝑔) ↔ (cod_a‘ℎ) = (dom_a‘𝐺)))
14	13	rabbidv 3440	. . . 4 ⊢ (𝑔 = 𝐺 → {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)} = {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝐺)})
15	14	opeliunxp2 5836	. . 3 ⊢ (⟨𝐺, 𝐹⟩ ∈ ∪ 𝑔 ∈ 𝐴 ({𝑔} × {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)}) ↔ (𝐺 ∈ 𝐴 ∧ 𝐹 ∈ {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝐺)}))
16		fveqeq2 6897	. . . . 5 ⊢ (ℎ = 𝐹 → ((cod_a‘ℎ) = (dom_a‘𝐺) ↔ (cod_a‘𝐹) = (dom_a‘𝐺)))
17	16	elrab 3682	. . . 4 ⊢ (𝐹 ∈ {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝐺)} ↔ (𝐹 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)))
18	17	anbi2i 623	. . 3 ⊢ ((𝐺 ∈ 𝐴 ∧ 𝐹 ∈ {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝐺)}) ↔ (𝐺 ∈ 𝐴 ∧ (𝐹 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺))))
19		an12 643	. . . 4 ⊢ ((𝐺 ∈ 𝐴 ∧ (𝐹 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺))) ↔ (𝐹 ∈ 𝐴 ∧ (𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺))))
20		3anass 1095	. . . 4 ⊢ ((𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)) ↔ (𝐹 ∈ 𝐴 ∧ (𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺))))
21	19, 20	bitr4i 277	. . 3 ⊢ ((𝐺 ∈ 𝐴 ∧ (𝐹 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺))) ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)))
22	15, 18, 21	3bitri 296	. 2 ⊢ (⟨𝐺, 𝐹⟩ ∈ ∪ 𝑔 ∈ 𝐴 ({𝑔} × {ℎ ∈ 𝐴 ∣ (cod_a‘ℎ) = (dom_a‘𝑔)}) ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)))
23	1, 11, 22	3bitri 296	1 ⊢ (𝐺dom · 𝐹 ↔ (𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ (cod_a‘𝐹) = (dom_a‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 {crab 3432 Vcvv 3474 {csn 4627 ⟨cop 4633 ⟨cotp 4635 ∪ ciun 4996 class class class wbr 5147 × cxp 5673 dom cdm 5675 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 2^nd c2nd 7970 compcco 17205 dom_acdoma 17966 cod_accoda 17967 Arrowcarw 17968 comp_accoa 18000

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-ot 4636 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7971 df-2nd 7972 df-arw 17973 df-coa 18002

This theorem is referenced by: homdmcoa 18013 coapm 18017

W3C validator