Metamath Proof Explorer

Theorem dmcosseq

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

Ref Expression
Assertion dmcosseq ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ A ∘ B = dom ⁡ B

Proof

Step Hyp Ref Expression
1 dmcoss ⊢ dom ⁡ A ∘ B ⊆ dom ⁡ B
2 1 a1i ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ A ∘ B ⊆ dom ⁡ B
3 ssel ⊢ ran ⁡ B ⊆ dom ⁡ A → y ∈ ran ⁡ B → y ∈ dom ⁡ A
4 vex ⊢ y ∈ V
5 4 elrn ⊢ y ∈ ran ⁡ B ↔ ∃ x x B y
6 4 eldm ⊢ y ∈ dom ⁡ A ↔ ∃ z y A z
7 5 6 imbi12i ⊢ y ∈ ran ⁡ B → y ∈ dom ⁡ A ↔ ∃ x x B y → ∃ z y A z
8 breq1 ⊢ x = z → x B y ↔ z B y
9 8 19.8aw ⊢ x B y → ∃ x x B y
10 9 imim1i ⊢ ∃ x x B y → ∃ z y A z → x B y → ∃ z y A z
11 pm3.2 ⊢ x B y → y A z → x B y ∧ y A z
12 11 eximdv ⊢ x B y → ∃ z y A z → ∃ z x B y ∧ y A z
13 10 12 sylcom ⊢ ∃ x x B y → ∃ z y A z → x B y → ∃ z x B y ∧ y A z
14 7 13 sylbi ⊢ y ∈ ran ⁡ B → y ∈ dom ⁡ A → x B y → ∃ z x B y ∧ y A z
15 3 14 syl ⊢ ran ⁡ B ⊆ dom ⁡ A → x B y → ∃ z x B y ∧ y A z
16 15 eximdv ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ y ∃ z x B y ∧ y A z
17 breq2 ⊢ y = w → x B y ↔ x B w
18 breq1 ⊢ y = w → y A z ↔ w A z
19 17 18 anbi12d ⊢ y = w → x B y ∧ y A z ↔ x B w ∧ w A z
20 19 excomimw ⊢ ∃ y ∃ z x B y ∧ y A z → ∃ z ∃ y x B y ∧ y A z
21 16 20 syl6 ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z ∃ y x B y ∧ y A z
22 vex ⊢ x ∈ V
23 vex ⊢ z ∈ V
24 22 23 opelco ⊢ x z ∈ A ∘ B ↔ ∃ y x B y ∧ y A z
25 24 exbii ⊢ ∃ z x z ∈ A ∘ B ↔ ∃ z ∃ y x B y ∧ y A z
26 21 25 imbitrrdi ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z x z ∈ A ∘ B
27 22 eldm ⊢ x ∈ dom ⁡ B ↔ ∃ y x B y
28 22 eldm2 ⊢ x ∈ dom ⁡ A ∘ B ↔ ∃ z x z ∈ A ∘ B
29 26 27 28 3imtr4g ⊢ ran ⁡ B ⊆ dom ⁡ A → x ∈ dom ⁡ B → x ∈ dom ⁡ A ∘ B
30 29 ssrdv ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ B ⊆ dom ⁡ A ∘ B
31 2 30 eqssd ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ A ∘ B = dom ⁡ B