Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brdom3.2 | |
|
Assertion | brdom3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brdom3.2 | |
|
2 | reldom | |
|
3 | 2 | brrelex1i | |
4 | 0sdomg | |
|
5 | 3 4 | syl | |
6 | df-ne | |
|
7 | 5 6 | bitrdi | |
8 | 7 | biimpar | |
9 | fodomr | |
|
10 | 9 | ancoms | |
11 | 8 10 | syldan | |
12 | pm5.6 | |
|
13 | 11 12 | mpbi | |
14 | br0 | |
|
15 | 14 | nex | |
16 | exmo | |
|
17 | 15 16 | mtpor | |
18 | 17 | ax-gen | |
19 | rzal | |
|
20 | 0ex | |
|
21 | breq | |
|
22 | 21 | mobidv | |
23 | 22 | albidv | |
24 | breq | |
|
25 | 24 | rexbidv | |
26 | 25 | ralbidv | |
27 | 23 26 | anbi12d | |
28 | 20 27 | spcev | |
29 | 18 19 28 | sylancr | |
30 | fofun | |
|
31 | dffun6 | |
|
32 | 31 | simprbi | |
33 | 30 32 | syl | |
34 | dffo4 | |
|
35 | 34 | simprbi | |
36 | 33 35 | jca | |
37 | 36 | eximi | |
38 | 29 37 | jaoi | |
39 | 13 38 | syl | |
40 | inss1 | |
|
41 | 40 | ssbri | |
42 | 41 | moimi | |
43 | 42 | alimi | |
44 | relinxp | |
|
45 | dffun6 | |
|
46 | 44 45 | mpbiran | |
47 | 43 46 | sylibr | |
48 | 47 | funfnd | |
49 | rninxp | |
|
50 | 49 | biimpri | |
51 | 48 50 | anim12i | |
52 | df-fo | |
|
53 | 51 52 | sylibr | |
54 | vex | |
|
55 | 54 | inex1 | |
56 | 55 | dmex | |
57 | 56 | fodom | |
58 | inss2 | |
|
59 | dmss | |
|
60 | 58 59 | ax-mp | |
61 | dmxpss | |
|
62 | 60 61 | sstri | |
63 | ssdomg | |
|
64 | 1 62 63 | mp2 | |
65 | domtr | |
|
66 | 64 65 | mpan2 | |
67 | 53 57 66 | 3syl | |
68 | 67 | exlimiv | |
69 | 39 68 | impbii | |