This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-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 breq1 
 |-  ( x = z -> ( x B y <-> z B y ) )
9 8 19.8aw 
 |-  ( x B y -> E. x x B y )
10 9 imim1i 
 |-  ( ( E. x x B y -> E. z y A z ) -> ( x B y -> E. z y A z ) )
11 pm3.2 
 |-  ( x B y -> ( y A z -> ( x B y /\ y A z ) ) )
12 11 eximdv 
 |-  ( x B y -> ( E. z y A z -> E. z ( x B y /\ y A z ) ) )
13 10 12 sylcom 
 |-  ( ( E. x x B y -> E. z y A z ) -> ( x B y -> E. z ( x B y /\ y A z ) ) )
14 7 13 sylbi 
 |-  ( ( y e. ran B -> y e. dom A ) -> ( x B y -> E. z ( x B y /\ y A z ) ) )
15 3 14 syl 
 |-  ( ran B C_ dom A -> ( x B y -> E. z ( x B y /\ y A z ) ) )
16 15 eximdv 
 |-  ( ran B C_ dom A -> ( E. y x B y -> E. y E. z ( x B y /\ y A z ) ) )
17 breq2 
 |-  ( y = w -> ( x B y <-> x B w ) )
18 breq1 
 |-  ( y = w -> ( y A z <-> w A z ) )
19 17 18 anbi12d 
 |-  ( y = w -> ( ( x B y /\ y A z ) <-> ( x B w /\ w A z ) ) )
20 19 excomimw 
 |-  ( E. y E. z ( x B y /\ y A z ) -> E. z E. y ( x B y /\ y A z ) )
21 16 20 syl6 
 |-  ( ran B C_ dom A -> ( E. y x B y -> E. z E. y ( x B y /\ y A z ) ) )
22 vex 
 |-  x e. _V
23 vex 
 |-  z e. _V
24 22 23 opelco 
 |-  ( <. x , z >. e. ( A o. B ) <-> E. y ( x B y /\ y A z ) )
25 24 exbii 
 |-  ( E. z <. x , z >. e. ( A o. B ) <-> E. z E. y ( x B y /\ y A z ) )
26 21 25 imbitrrdi 
 |-  ( ran B C_ dom A -> ( E. y x B y -> E. z <. x , z >. e. ( A o. B ) ) )
27 22 eldm 
 |-  ( x e. dom B <-> E. y x B y )
28 22 eldm2 
 |-  ( x e. dom ( A o. B ) <-> E. z <. x , z >. e. ( A o. B ) )
29 26 27 28 3imtr4g 
 |-  ( ran B C_ dom A -> ( x e. dom B -> x e. dom ( A o. B ) ) )
30 29 ssrdv 
 |-  ( ran B C_ dom A -> dom B C_ dom ( A o. B ) )
31 2 30 eqssd 
 |-  ( ran B C_ dom A -> dom ( A o. B ) = dom B )