Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brdom3.2 | |
|
Assertion | brdom5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brdom3.2 | |
|
2 | 1 | brdom3 | |
3 | alral | |
|
4 | 3 | anim1i | |
5 | 4 | eximi | |
6 | 2 5 | sylbi | |
7 | inss2 | |
|
8 | dmss | |
|
9 | 7 8 | ax-mp | |
10 | dmxpss | |
|
11 | 9 10 | sstri | |
12 | 11 | sseli | |
13 | inss1 | |
|
14 | 13 | ssbri | |
15 | 14 | moimi | |
16 | 12 15 | imim12i | |
17 | 16 | ralimi2 | |
18 | relinxp | |
|
19 | 17 18 | jctil | |
20 | dffun7 | |
|
21 | 19 20 | sylibr | |
22 | 21 | funfnd | |
23 | rninxp | |
|
24 | 23 | biimpri | |
25 | 22 24 | anim12i | |
26 | df-fo | |
|
27 | 25 26 | sylibr | |
28 | vex | |
|
29 | 28 | inex1 | |
30 | 29 | dmex | |
31 | 30 | fodom | |
32 | ssdomg | |
|
33 | 1 11 32 | mp2 | |
34 | domtr | |
|
35 | 33 34 | mpan2 | |
36 | 27 31 35 | 3syl | |
37 | 36 | exlimiv | |
38 | 6 37 | impbii | |