Metamath Proof Explorer

Theorem dmcosseq

Description: Domain of a composition. (Contributed by NM, 28-May-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025)

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 breq2 
 |-  ( y = w -> ( x B y <-> x B w ) )
17 breq1 
 |-  ( y = w -> ( y A z <-> w A z ) )
18 16 17 anbi12d 
 |-  ( y = w -> ( ( x B y /\ y A z ) <-> ( x B w /\ w A z ) ) )
19 18 excomimw 
 |-  ( E. y E. z ( x B y /\ y A z ) -> E. z E. y ( x B y /\ y A z ) )
20 15 19 syl6 
 |-  ( ran B C_ dom A -> ( E. y x B y -> E. z E. y ( x B y /\ y A z ) ) )
21 vex 
 |-  x e. _V
22 vex 
 |-  z e. _V
23 21 22 opelco 
 |-  ( <. x , z >. e. ( A o. B ) <-> E. y ( x B y /\ y A z ) )
24 23 exbii 
 |-  ( E. z <. x , z >. e. ( A o. B ) <-> E. z E. y ( x B y /\ y A z ) )
25 20 24 imbitrrdi 
 |-  ( ran B C_ dom A -> ( E. y x B y -> E. z <. x , z >. e. ( A o. B ) ) )
26 21 eldm 
 |-  ( x e. dom B <-> E. y x B y )
27 21 eldm2 
 |-  ( x e. dom ( A o. B ) <-> E. z <. x , z >. e. ( A o. B ) )
28 25 26 27 3imtr4g 
 |-  ( ran B C_ dom A -> ( x e. dom B -> x e. dom ( A o. B ) ) )
29 28 ssrdv 
 |-  ( ran B C_ dom A -> dom B C_ dom ( A o. B ) )
30 2 29 eqssd 
 |-  ( ran B C_ dom A -> dom ( A o. B ) = dom B )