Metamath Proof Explorer

Theorem dmcosseqOLD

Description: Obsolete version of dmcosseq as of 23-Jun-2025. (Contributed by NM, 28-May-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dmcosseqOLD 
|- ( 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 imbitrrdi 
 |-  ( 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 imbitrrdi 
 |-  ( 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 )