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

Proof

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