Theorem dmcosseq

Description: Domain of a composition. (Contributed by NM, 28-May-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	dmcosseq	|- ( ran B C_ dom A -> dom ( A o. B ) = dom B )

Proof

Step	Hyp	Ref	Expression
1		dmcoss	|- dom ( A o. B ) C_ dom B
2	1	a1i	|- ( ran B C_ dom A -> dom ( A o. B ) C_ dom B )
3		ssel	|- ( ran B C_ dom A -> ( y e. ran B -> y e. dom A ) )
4		vex	|- y e. _V
5	4	elrn	|- ( y e. ran B <-> E. x x B y )
6	4	eldm	|- ( y e. dom A <-> E. z y A z )
7	5 6	imbi12i	|- ( ( y e. ran B -> y e. dom A ) <-> ( E. x x B y -> E. z y A z ) )
8		19.8a	|- ( x B y -> E. x x B y )
9	8	imim1i	|- ( ( E. x x B y -> E. z y A z ) -> ( x B y -> E. z y A z ) )
10		pm3.2	|- ( x B y -> ( y A z -> ( x B y /\ y A z ) ) )
11	10	eximdv	|- ( x B y -> ( E. z y A z -> E. z ( x B y /\ y A z ) ) )
12	9 11	sylcom	|- ( ( E. x x B y -> E. z y A z ) -> ( x B y -> E. z ( x B y /\ y A z ) ) )
13	7 12	sylbi	|- ( ( y e. ran B -> y e. dom A ) -> ( x B y -> E. z ( x B y /\ y A z ) ) )
14	3 13	syl	|- ( ran B C_ dom A -> ( x B y -> E. z ( x B y /\ y A z ) ) )
15	14	eximdv	|- ( ran B C_ dom A -> ( E. y x B y -> E. y E. z ( x B y /\ y A z ) ) )
16		excom	|- ( E. z E. y ( x B y /\ y A z ) <-> E. y E. z ( x B y /\ y A z ) )
17	15 16	syl6ibr	|- ( ran B C_ dom A -> ( E. y x B y -> E. z E. y ( x B y /\ y A z ) ) )
18		vex	|- x e. _V
19		vex	|- z e. _V
20	18 19	opelco	|- ( <. x , z >. e. ( A o. B ) <-> E. y ( x B y /\ y A z ) )
21	20	exbii	|- ( E. z <. x , z >. e. ( A o. B ) <-> E. z E. y ( x B y /\ y A z ) )
22	17 21	syl6ibr	|- ( ran B C_ dom A -> ( E. y x B y -> E. z <. x , z >. e. ( A o. B ) ) )
23	18	eldm	|- ( x e. dom B <-> E. y x B y )
24	18	eldm2	|- ( x e. dom ( A o. B ) <-> E. z <. x , z >. e. ( A o. B ) )
25	22 23 24	3imtr4g	|- ( ran B C_ dom A -> ( x e. dom B -> x e. dom ( A o. B ) ) )
26	25	ssrdv	|- ( ran B C_ dom A -> dom B C_ dom ( A o. B ) )
27	2 26	eqssd	|- ( ran B C_ dom A -> dom ( A o. B ) = dom B )