Metamath Proof Explorer


Theorem brdom3

Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)

Ref Expression
Hypothesis brdom3.2 BV
Assertion brdom3 ABfx*yxfyxAyByfx

Proof

Step Hyp Ref Expression
1 brdom3.2 BV
2 reldom Rel
3 2 brrelex1i ABAV
4 0sdomg AVAA
5 3 4 syl ABAA
6 df-ne A¬A=
7 5 6 bitrdi ABA¬A=
8 7 biimpar AB¬A=A
9 fodomr AABff:BontoA
10 9 ancoms ABAff:BontoA
11 8 10 syldan AB¬A=ff:BontoA
12 pm5.6 AB¬A=ff:BontoAABA=ff:BontoA
13 11 12 mpbi ABA=ff:BontoA
14 br0 ¬xy
15 14 nex ¬yxy
16 exmo yxy*yxy
17 15 16 mtpor *yxy
18 17 ax-gen x*yxy
19 rzal A=xAyByx
20 0ex V
21 breq f=xfyxy
22 21 mobidv f=*yxfy*yxy
23 22 albidv f=x*yxfyx*yxy
24 breq f=yfxyx
25 24 rexbidv f=yByfxyByx
26 25 ralbidv f=xAyByfxxAyByx
27 23 26 anbi12d f=x*yxfyxAyByfxx*yxyxAyByx
28 20 27 spcev x*yxyxAyByxfx*yxfyxAyByfx
29 18 19 28 sylancr A=fx*yxfyxAyByfx
30 fofun f:BontoAFunf
31 dffun6 FunfRelfx*yxfy
32 31 simprbi Funfx*yxfy
33 30 32 syl f:BontoAx*yxfy
34 dffo4 f:BontoAf:BAxAyByfx
35 34 simprbi f:BontoAxAyByfx
36 33 35 jca f:BontoAx*yxfyxAyByfx
37 36 eximi ff:BontoAfx*yxfyxAyByfx
38 29 37 jaoi A=ff:BontoAfx*yxfyxAyByfx
39 13 38 syl ABfx*yxfyxAyByfx
40 inss1 fB×Af
41 40 ssbri xfB×Ayxfy
42 41 moimi *yxfy*yxfB×Ay
43 42 alimi x*yxfyx*yxfB×Ay
44 relinxp RelfB×A
45 dffun6 FunfB×ARelfB×Ax*yxfB×Ay
46 44 45 mpbiran FunfB×Ax*yxfB×Ay
47 43 46 sylibr x*yxfyFunfB×A
48 47 funfnd x*yxfyfB×AFndomfB×A
49 rninxp ranfB×A=AxAyByfx
50 49 biimpri xAyByfxranfB×A=A
51 48 50 anim12i x*yxfyxAyByfxfB×AFndomfB×AranfB×A=A
52 df-fo fB×A:domfB×AontoAfB×AFndomfB×AranfB×A=A
53 51 52 sylibr x*yxfyxAyByfxfB×A:domfB×AontoA
54 vex fV
55 54 inex1 fB×AV
56 55 dmex domfB×AV
57 56 fodom fB×A:domfB×AontoAAdomfB×A
58 inss2 fB×AB×A
59 dmss fB×AB×AdomfB×AdomB×A
60 58 59 ax-mp domfB×AdomB×A
61 dmxpss domB×AB
62 60 61 sstri domfB×AB
63 ssdomg BVdomfB×ABdomfB×AB
64 1 62 63 mp2 domfB×AB
65 domtr AdomfB×AdomfB×ABAB
66 64 65 mpan2 AdomfB×AAB
67 53 57 66 3syl x*yxfyxAyByfxAB
68 67 exlimiv fx*yxfyxAyByfxAB
69 39 68 impbii ABfx*yxfyxAyByfx