This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmcoss

Description: Domain of a composition. Theorem 21 of Suppes p. 63. (Contributed by NM, 19-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-2025)

Ref Expression
Assertion dmcoss ⊢ dom ⁡ A ∘ B ⊆ dom ⁡ B

Proof

Step Hyp Ref Expression
1 exsimpl ⊢ ∃ z x B z ∧ z A y → ∃ z x B z
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 opelco ⊢ x y ∈ A ∘ B ↔ ∃ z x B z ∧ z A y
5 breq2 ⊢ y = z → x B y ↔ x B z
6 5 cbvexvw ⊢ ∃ y x B y ↔ ∃ z x B z
7 1 4 6 3imtr4i ⊢ x y ∈ A ∘ B → ∃ y x B y
8 7 eximi ⊢ ∃ y x y ∈ A ∘ B → ∃ y ∃ y x B y
9 5 exexw ⊢ ∃ y x B y ↔ ∃ y ∃ y x B y
10 8 9 sylibr ⊢ ∃ y x y ∈ A ∘ B → ∃ y x B y
11 2 eldm2 ⊢ x ∈ dom ⁡ A ∘ B ↔ ∃ y x y ∈ A ∘ B
12 2 eldm ⊢ x ∈ dom ⁡ B ↔ ∃ y x B y
13 10 11 12 3imtr4i ⊢ x ∈ dom ⁡ A ∘ B → x ∈ dom ⁡ B
14 13 ssriv ⊢ dom ⁡ A ∘ B ⊆ dom ⁡ B