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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmcoss | |
|
2 | 1 | a1i | |
3 | ssel | |
|
4 | vex | |
|
5 | 4 | elrn | |
6 | 4 | eldm | |
7 | 5 6 | imbi12i | |
8 | 19.8a | |
|
9 | 8 | imim1i | |
10 | pm3.2 | |
|
11 | 10 | eximdv | |
12 | 9 11 | sylcom | |
13 | 7 12 | sylbi | |
14 | 3 13 | syl | |
15 | 14 | eximdv | |
16 | breq2 | |
|
17 | breq1 | |
|
18 | 16 17 | anbi12d | |
19 | 18 | excomimw | |
20 | 15 19 | syl6 | |
21 | vex | |
|
22 | vex | |
|
23 | 21 22 | opelco | |
24 | 23 | exbii | |
25 | 20 24 | imbitrrdi | |
26 | 21 | eldm | |
27 | 21 | eldm2 | |
28 | 25 26 27 | 3imtr4g | |
29 | 28 | ssrdv | |
30 | 2 29 | eqssd | |