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 𝐵