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)

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 19.8a ⊢ x B y → ∃ x x B y
9 8 imim1i ⊢ ∃ x x B y → ∃ z y A z → x B y → ∃ z y A z
10 pm3.2 ⊢ x B y → y A z → x B y ∧ y A z
11 10 eximdv ⊢ x B y → ∃ z y A z → ∃ z x B y ∧ y A z
12 9 11 sylcom ⊢ ∃ x x B y → ∃ z y A z → x B y → ∃ z x B y ∧ y A z
13 7 12 sylbi ⊢ y ∈ ran ⁡ B → y ∈ dom ⁡ A → x B y → ∃ z x B y ∧ y A z
14 3 13 syl ⊢ ran ⁡ B ⊆ dom ⁡ A → x B y → ∃ z x B y ∧ y A z
15 14 eximdv ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ y ∃ z x B y ∧ y A z
16 breq2 ⊢ y = w → x B y ↔ x B w
17 breq1 ⊢ y = w → y A z ↔ w A z
18 16 17 anbi12d ⊢ y = w → x B y ∧ y A z ↔ x B w ∧ w A z
19 18 excomimw ⊢ ∃ y ∃ z x B y ∧ y A z → ∃ z ∃ y x B y ∧ y A z
20 15 19 syl6 ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z ∃ y x B y ∧ y A z
21 vex ⊢ x ∈ V
22 vex ⊢ z ∈ V
23 21 22 opelco ⊢ x z ∈ A ∘ B ↔ ∃ y x B y ∧ y A z
24 23 exbii ⊢ ∃ z x z ∈ A ∘ B ↔ ∃ z ∃ y x B y ∧ y A z
25 20 24 imbitrrdi ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z x z ∈ A ∘ B
26 21 eldm ⊢ x ∈ dom ⁡ B ↔ ∃ y x B y
27 21 eldm2 ⊢ x ∈ dom ⁡ A ∘ B ↔ ∃ z x z ∈ A ∘ B
28 25 26 27 3imtr4g ⊢ ran ⁡ B ⊆ dom ⁡ A → x ∈ dom ⁡ B → x ∈ dom ⁡ A ∘ B
29 28 ssrdv ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ B ⊆ dom ⁡ A ∘ B
30 2 29 eqssd ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ A ∘ B = dom ⁡ B