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 ranBdomAdomAB=domB

Proof

Step Hyp Ref Expression
1 dmcoss domABdomB
2 1 a1i ranBdomAdomABdomB
3 ssel ranBdomAyranBydomA
4 vex yV
5 4 elrn yranBxxBy
6 4 eldm ydomAzyAz
7 5 6 imbi12i yranBydomAxxByzyAz
8 19.8a xByxxBy
9 8 imim1i xxByzyAzxByzyAz
10 pm3.2 xByyAzxByyAz
11 10 eximdv xByzyAzzxByyAz
12 9 11 sylcom xxByzyAzxByzxByyAz
13 7 12 sylbi yranBydomAxByzxByyAz
14 3 13 syl ranBdomAxByzxByyAz
15 14 eximdv ranBdomAyxByyzxByyAz
16 breq2 y=wxByxBw
17 breq1 y=wyAzwAz
18 16 17 anbi12d y=wxByyAzxBwwAz
19 18 excomimw yzxByyAzzyxByyAz
20 15 19 syl6 ranBdomAyxByzyxByyAz
21 vex xV
22 vex zV
23 21 22 opelco xzAByxByyAz
24 23 exbii zxzABzyxByyAz
25 20 24 imbitrrdi ranBdomAyxByzxzAB
26 21 eldm xdomByxBy
27 21 eldm2 xdomABzxzAB
28 25 26 27 3imtr4g ranBdomAxdomBxdomAB
29 28 ssrdv ranBdomAdomBdomAB
30 2 29 eqssd ranBdomAdomAB=domB