Metamath Proof Explorer

Theorem dmcosseq

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

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 excom ⊢ ∃ z ∃ y x B y ∧ y A z ↔ ∃ y ∃ z x B y ∧ y A z
17 15 16 imbitrrdi ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z ∃ y x B y ∧ y A z
18 vex ⊢ x ∈ V
19 vex ⊢ z ∈ V
20 18 19 opelco ⊢ x z ∈ A ∘ B ↔ ∃ y x B y ∧ y A z
21 20 exbii ⊢ ∃ z x z ∈ A ∘ B ↔ ∃ z ∃ y x B y ∧ y A z
22 17 21 imbitrrdi ⊢ ran ⁡ B ⊆ dom ⁡ A → ∃ y x B y → ∃ z x z ∈ A ∘ B
23 18 eldm ⊢ x ∈ dom ⁡ B ↔ ∃ y x B y
24 18 eldm2 ⊢ x ∈ dom ⁡ A ∘ B ↔ ∃ z x z ∈ A ∘ B
25 22 23 24 3imtr4g ⊢ ran ⁡ B ⊆ dom ⁡ A → x ∈ dom ⁡ B → x ∈ dom ⁡ A ∘ B
26 25 ssrdv ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ B ⊆ dom ⁡ A ∘ B
27 2 26 eqssd ⊢ ran ⁡ B ⊆ dom ⁡ A → dom ⁡ A ∘ B = dom ⁡ B