Theorem dmcosseq 5959

Description: Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-11 2194. (Revised by BTernaryTau, 23-Jun-2025.) Avoid ax-10 2178 and ax-12 2215. (Revised by TM, 31-Dec-2025.)

Assertion

Ref	Expression
dmcosseq	⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵)

Proof of Theorem dmcosseq

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmcoss 5956	. . 3 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵
2	1	a1i 11	. 2 ⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵)
3		ssel 3933	. . . . . . . 8 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴))
4		vex 3461	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
5	4	elrn 5874	. . . . . . . . . 10 ⊢ (𝑦 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝑦)
6	4	eldm 5881	. . . . . . . . . 10 ⊢ (𝑦 ∈ dom 𝐴 ↔ ∃𝑧 𝑦𝐴𝑧)
7	5, 6	imbi12i 353	. . . . . . . . 9 ⊢ ((𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴) ↔ (∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧))
8		breq1 5108	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑧𝐵𝑦))
9	8	19.8aw 2075	. . . . . . . . . . 11 ⊢ (𝑥𝐵𝑦 → ∃𝑥 𝑥𝐵𝑦)
10	9	imim1i 64	. . . . . . . . . 10 ⊢ ((∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧) → (𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧))
11		pm3.2 474	. . . . . . . . . . 11 ⊢ (𝑥𝐵𝑦 → (𝑦𝐴𝑧 → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
12	11	eximdv 1940	. . . . . . . . . 10 ⊢ (𝑥𝐵𝑦 → (∃𝑧 𝑦𝐴𝑧 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
13	10, 12	sylcom 31	. . . . . . . . 9 ⊢ ((∃𝑥 𝑥𝐵𝑦 → ∃𝑧 𝑦𝐴𝑧) → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
14	7, 13	sylbi 220	. . . . . . . 8 ⊢ ((𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴) → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
15	3, 14	syl 18	. . . . . . 7 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (𝑥𝐵𝑦 → ∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
16	15	eximdv 1940	. . . . . 6 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑦∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
17		breq2 5109	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑤))
18		breq1 5108	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑦𝐴𝑧 ↔ 𝑤𝐴𝑧))
19	17, 18	anbi12d 643	. . . . . . 7 ⊢ (𝑦 = 𝑤 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑤 ∧ 𝑤𝐴𝑧)))
20	19	excomimw 2067	. . . . . 6 ⊢ (∃𝑦∃𝑧(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → ∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
21	16, 20	syl6 36	. . . . 5 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
22		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
23		vex 3461	. . . . . . 7 ⊢ 𝑧 ∈ V
24	22, 23	opelco 5848	. . . . . 6 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
25	24	exbii 1871	. . . . 5 ⊢ (∃𝑧⟨𝑥, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
26	21, 25	imbitrrdi 255	. . . 4 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (∃𝑦 𝑥𝐵𝑦 → ∃𝑧⟨𝑥, 𝑧⟩ ∈ (𝐴 ∘ 𝐵)))
27	22	eldm 5881	. . . 4 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
28	22	eldm2 5882	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑧⟨𝑥, 𝑧⟩ ∈ (𝐴 ∘ 𝐵))
29	26, 27, 28	3imtr4g 299	. . 3 ⊢ (ran 𝐵 ⊆ dom 𝐴 → (𝑥 ∈ dom 𝐵 → 𝑥 ∈ dom (𝐴 ∘ 𝐵)))
30	29	ssrdv 3945	. 2 ⊢ (ran 𝐵 ⊆ dom 𝐴 → dom 𝐵 ⊆ dom (𝐴 ∘ 𝐵))
31	2, 30	eqssd 3956	1 ⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ⊆ wss 3907  ⟨cop 4591   class class class wbr 5105  dom cdm 5652  ran crn 5653   ∘ ccom 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663

This theorem is referenced by:  dmcoeq  5961  cycpmconjv  33375  dmcoss3  39054  comptiunov2i  44294  dvsinax  46485  hoicvr  47120  chnsubseqwl  47453  fnresfnco  47633