Theorem dmcosseq 4546

Description: Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
dmcosseq	⊢ (ran B ⊆ dom A → dom (A ∘ B) = dom B)

Proof of Theorem dmcosseq

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmcoss 4544	. . 3 ⊢ dom (A ∘ B) ⊆ dom B
2	1	a1i 9	. 2 ⊢ (ran B ⊆ dom A → dom (A ∘ B) ⊆ dom B)
3		ssel 2933	. . . . . . . 8 ⊢ (ran B ⊆ dom A → (y ∈ ran B → y ∈ dom A))
4		vex 2554	. . . . . . . . . . 11 ⊢ y ∈ V
5	4	elrn 4520	. . . . . . . . . 10 ⊢ (y ∈ ran B ↔ ∃x xBy)
6	4	eldm 4475	. . . . . . . . . 10 ⊢ (y ∈ dom A ↔ ∃z yAz)
7	5, 6	imbi12i 228	. . . . . . . . 9 ⊢ ((y ∈ ran B → y ∈ dom A) ↔ (∃x xBy → ∃z yAz))
8		19.8a 1479	. . . . . . . . . . 11 ⊢ (xBy → ∃x xBy)
9	8	imim1i 54	. . . . . . . . . 10 ⊢ ((∃x xBy → ∃z yAz) → (xBy → ∃z yAz))
10		pm3.2 126	. . . . . . . . . . 11 ⊢ (xBy → (yAz → (xBy ∧ yAz)))
11	10	eximdv 1757	. . . . . . . . . 10 ⊢ (xBy → (∃z yAz → ∃z(xBy ∧ yAz)))
12	9, 11	sylcom 25	. . . . . . . . 9 ⊢ ((∃x xBy → ∃z yAz) → (xBy → ∃z(xBy ∧ yAz)))
13	7, 12	sylbi 114	. . . . . . . 8 ⊢ ((y ∈ ran B → y ∈ dom A) → (xBy → ∃z(xBy ∧ yAz)))
14	3, 13	syl 14	. . . . . . 7 ⊢ (ran B ⊆ dom A → (xBy → ∃z(xBy ∧ yAz)))
15	14	eximdv 1757	. . . . . 6 ⊢ (ran B ⊆ dom A → (∃y xBy → ∃y∃z(xBy ∧ yAz)))
16		excom 1551	. . . . . 6 ⊢ (∃z∃y(xBy ∧ yAz) ↔ ∃y∃z(xBy ∧ yAz))
17	15, 16	syl6ibr 151	. . . . 5 ⊢ (ran B ⊆ dom A → (∃y xBy → ∃z∃y(xBy ∧ yAz)))
18		vex 2554	. . . . . . 7 ⊢ x ∈ V
19		vex 2554	. . . . . . 7 ⊢ z ∈ V
20	18, 19	opelco 4450	. . . . . 6 ⊢ (⟨x, z⟩ ∈ (A ∘ B) ↔ ∃y(xBy ∧ yAz))
21	20	exbii 1493	. . . . 5 ⊢ (∃z⟨x, z⟩ ∈ (A ∘ B) ↔ ∃z∃y(xBy ∧ yAz))
22	17, 21	syl6ibr 151	. . . 4 ⊢ (ran B ⊆ dom A → (∃y xBy → ∃z⟨x, z⟩ ∈ (A ∘ B)))
23	18	eldm 4475	. . . 4 ⊢ (x ∈ dom B ↔ ∃y xBy)
24	18	eldm2 4476	. . . 4 ⊢ (x ∈ dom (A ∘ B) ↔ ∃z⟨x, z⟩ ∈ (A ∘ B))
25	22, 23, 24	3imtr4g 194	. . 3 ⊢ (ran B ⊆ dom A → (x ∈ dom B → x ∈ dom (A ∘ B)))
26	25	ssrdv 2945	. 2 ⊢ (ran B ⊆ dom A → dom B ⊆ dom (A ∘ B))
27	2, 26	eqssd 2956	1 ⊢ (ran B ⊆ dom A → dom (A ∘ B) = dom B)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  dom cdm 4288  ran crn 4289   ∘ ccom 4292

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299

This theorem is referenced by:  dmcoeq  4547  fnco  4950