Metamath Proof Explorer


Theorem brdom5

Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007)

Ref Expression
Hypothesis brdom3.2 BV
Assertion brdom5 ABfxB*yxfyxAyByfx

Proof

Step Hyp Ref Expression
1 brdom3.2 BV
2 1 brdom3 ABfx*yxfyxAyByfx
3 alral x*yxfyxB*yxfy
4 3 anim1i x*yxfyxAyByfxxB*yxfyxAyByfx
5 4 eximi fx*yxfyxAyByfxfxB*yxfyxAyByfx
6 2 5 sylbi ABfxB*yxfyxAyByfx
7 inss2 fB×AB×A
8 dmss fB×AB×AdomfB×AdomB×A
9 7 8 ax-mp domfB×AdomB×A
10 dmxpss domB×AB
11 9 10 sstri domfB×AB
12 11 sseli xdomfB×AxB
13 inss1 fB×Af
14 13 ssbri xfB×Ayxfy
15 14 moimi *yxfy*yxfB×Ay
16 12 15 imim12i xB*yxfyxdomfB×A*yxfB×Ay
17 16 ralimi2 xB*yxfyxdomfB×A*yxfB×Ay
18 relinxp RelfB×A
19 17 18 jctil xB*yxfyRelfB×AxdomfB×A*yxfB×Ay
20 dffun7 FunfB×ARelfB×AxdomfB×A*yxfB×Ay
21 19 20 sylibr xB*yxfyFunfB×A
22 21 funfnd xB*yxfyfB×AFndomfB×A
23 rninxp ranfB×A=AxAyByfx
24 23 biimpri xAyByfxranfB×A=A
25 22 24 anim12i xB*yxfyxAyByfxfB×AFndomfB×AranfB×A=A
26 df-fo fB×A:domfB×AontoAfB×AFndomfB×AranfB×A=A
27 25 26 sylibr xB*yxfyxAyByfxfB×A:domfB×AontoA
28 vex fV
29 28 inex1 fB×AV
30 29 dmex domfB×AV
31 30 fodom fB×A:domfB×AontoAAdomfB×A
32 ssdomg BVdomfB×ABdomfB×AB
33 1 11 32 mp2 domfB×AB
34 domtr AdomfB×AdomfB×ABAB
35 33 34 mpan2 AdomfB×AAB
36 27 31 35 3syl xB*yxfyxAyByfxAB
37 36 exlimiv fxB*yxfyxAyByfxAB
38 6 37 impbii ABfxB*yxfyxAyByfx