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

Metamath Proof Explorer

Theorem dmcossOLD

Description: Obsolete version of dmcosseq as of 31-Dec-2025. (Contributed by NM, 19-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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