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 ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵

Proof

Step Hyp Ref Expression
1 exsimpl ⊢ ( ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) → ∃ 𝑧 𝑥 𝐵 𝑧 )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
5 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐵 𝑦 ↔ 𝑥 𝐵 𝑧 ) )
6 5 cbvexvw ⊢ ( ∃ 𝑦 𝑥 𝐵 𝑦 ↔ ∃ 𝑧 𝑥 𝐵 𝑧 )
7 1 4 6 3imtr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) → ∃ 𝑦 𝑥 𝐵 𝑦 )
8 7 eximi ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) → ∃ 𝑦 ∃ 𝑦 𝑥 𝐵 𝑦 )
9 5 exexw ⊢ ( ∃ 𝑦 𝑥 𝐵 𝑦 ↔ ∃ 𝑦 ∃ 𝑦 𝑥 𝐵 𝑦 )
10 8 9 sylibr ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) → ∃ 𝑦 𝑥 𝐵 𝑦 )
11 2 eldm2 ⊢ ( 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
12 2 eldm ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 𝑥 𝐵 𝑦 )
13 10 11 12 3imtr4i ⊢ ( 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) → 𝑥 ∈ dom 𝐵 )
14 13 ssriv ⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵